Proof of Theorem 1stex
Step | Hyp | Ref
| Expression |
1 | | df1st2 4738 |
. 2
⋃1⋃1 k
k
k ∼
Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins2k Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck ∼ Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins3k SIk SIk Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck1 1c |
2 | | vvex 4109 |
. . . . . . . 8
|
3 | 2, 2 | xpkex 4289 |
. . . . . . 7
k
|
4 | 3, 2 | xpkex 4289 |
. . . . . 6
k
k
|
5 | | setconslem5 4735 |
. . . . . . 7
∼ Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins2k Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1c
|
6 | 5 | cnvkex 4287 |
. . . . . 6
k
∼ Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins2k Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1c
|
7 | 4, 6 | inex 4105 |
. . . . 5
k k
k
∼ Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins2k Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1c
|
8 | | ssetkex 4294 |
. . . . . . . . . . 11
Sk |
9 | 8 | ins3kex 4308 |
. . . . . . . . . 10
Ins3k Sk |
10 | 9 | ins2kex 4307 |
. . . . . . . . 9
Ins2k Ins3k Sk |
11 | | addcexlem 4382 |
. . . . . . . . . . . . . . . . . . . 20
Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1c
|
12 | | 1cex 4142 |
. . . . . . . . . . . . . . . . . . . . . 22
1c
|
13 | 12 | pw1ex 4303 |
. . . . . . . . . . . . . . . . . . . . 21
1
1c
|
14 | 13 | pw1ex 4303 |
. . . . . . . . . . . . . . . . . . . 20
1 1
1c
|
15 | 11, 14 | imakex 4300 |
. . . . . . . . . . . . . . . . . . 19
Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
|
16 | 15 | imagekex 4312 |
. . . . . . . . . . . . . . . . . 18
Imagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
|
17 | | nncex 4396 |
. . . . . . . . . . . . . . . . . . 19
Nn |
18 | 17, 2 | xpkex 4289 |
. . . . . . . . . . . . . . . . . 18
Nn k
|
19 | 16, 18 | inex 4105 |
. . . . . . . . . . . . . . . . 17
Imagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k |
20 | | idkex 4314 |
. . . . . . . . . . . . . . . . . 18
k
|
21 | 17 | complex 4104 |
. . . . . . . . . . . . . . . . . . 19
∼ Nn |
22 | 21, 2 | xpkex 4289 |
. . . . . . . . . . . . . . . . . 18
∼ Nn k
|
23 | 20, 22 | inex 4105 |
. . . . . . . . . . . . . . . . 17
k ∼ Nn k
|
24 | 19, 23 | unex 4106 |
. . . . . . . . . . . . . . . 16
Imagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k |
25 | 24 | imagekex 4312 |
. . . . . . . . . . . . . . 15
ImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k |
26 | 25 | cnvkex 4287 |
. . . . . . . . . . . . . 14
kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k |
27 | 26 | sikex 4297 |
. . . . . . . . . . . . 13
SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k |
28 | 8, 27 | cokex 4310 |
. . . . . . . . . . . 12
Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k |
29 | 28 | ins2kex 4307 |
. . . . . . . . . . 11
Ins2k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k |
30 | 29 | ins2kex 4307 |
. . . . . . . . . 10
Ins2k Ins2k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k |
31 | 8 | ins2kex 4307 |
. . . . . . . . . . . . . . 15
Ins2k Sk |
32 | 26, 8 | cokex 4310 |
. . . . . . . . . . . . . . . . . . . . . 22
kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk
|
33 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . 23
0c
|
34 | 33, 2 | xpkex 4289 |
. . . . . . . . . . . . . . . . . . . . . 22
0c k
|
35 | 32, 34 | unex 4106 |
. . . . . . . . . . . . . . . . . . . . 21
kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k |
36 | 35 | ins3kex 4308 |
. . . . . . . . . . . . . . . . . . . 20
Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k |
37 | 31, 36 | symdifex 4108 |
. . . . . . . . . . . . . . . . . . 19
Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k |
38 | 37, 14 | imakex 4300 |
. . . . . . . . . . . . . . . . . 18
Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1c |
39 | 38 | complex 4104 |
. . . . . . . . . . . . . . . . 17
∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1c |
40 | 39 | sikex 4297 |
. . . . . . . . . . . . . . . 16
SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1c |
41 | 40 | ins3kex 4308 |
. . . . . . . . . . . . . . 15
Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1c |
42 | 31, 41 | inex 4105 |
. . . . . . . . . . . . . 14
Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1c |
43 | 42, 14 | imakex 4300 |
. . . . . . . . . . . . 13
Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1c |
44 | 43 | sikex 4297 |
. . . . . . . . . . . 12
SIk Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1c |
45 | 44 | sikex 4297 |
. . . . . . . . . . 11
SIk SIk Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1c |
46 | 45 | ins3kex 4308 |
. . . . . . . . . 10
Ins3k SIk SIk Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1c |
47 | 30, 46 | unex 4106 |
. . . . . . . . 9
Ins2k Ins2k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins3k SIk SIk Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1c |
48 | 10, 47 | symdifex 4108 |
. . . . . . . 8
Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins3k SIk SIk Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1c |
49 | 14 | pw1ex 4303 |
. . . . . . . . 9
1 1 1
1c
|
50 | 49 | pw1ex 4303 |
. . . . . . . 8
1 1 1 1
1c
|
51 | 48, 50 | imakex 4300 |
. . . . . . 7
Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins3k SIk SIk Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1c
|
52 | 51 | complex 4104 |
. . . . . 6
∼ Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins3k SIk SIk Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1c
|
53 | 52, 13 | imakex 4300 |
. . . . 5
∼ Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins3k SIk SIk Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck1 1c
|
54 | 7, 53 | imakex 4300 |
. . . 4
k k
k
∼ Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins2k Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck ∼ Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins3k SIk SIk Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck1 1c
|
55 | 54 | uni1ex 4293 |
. . 3
⋃1 k k
k
∼ Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins2k Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck ∼ Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins3k SIk SIk Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck1 1c
|
56 | 55 | uni1ex 4293 |
. 2
⋃1⋃1 k
k
k ∼
Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins2k Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck ∼ Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k Ins3k SIk SIk Ins2k Sk Ins3k SIk ∼ Ins2k Sk Ins3k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k Sk 0c k k1 1 1ck1 1 1ck1 1 1 1 1ck1 1c
|
57 | 1, 56 | eqeltri 2423 |
1
|