let FSG be Friendship_Graph; ( not FSG is empty implies FSG is with_universal_friend )
set F = field FSG;
defpred S1[ FinSequence] means for i being Nat st 1 <= i & i < len $1 holds
[($1 . i),($1 . (i + 1))] in FSG;
deffunc H1( object ) -> set = Im (FSG,$1);
assume A1:
( not FSG is empty & FSG is without_universal_friend )
; contradiction
then consider x being object such that
A2:
x in field FSG
by XBOOLE_0:def 1;
reconsider F = field FSG as non empty finite set by A2;
set m = card (Im (FSG,x));
reconsider m1 = (card (Im (FSG,x))) - 1 as Nat by Th10, A1, A2, NAT_1:20;
m1 + 1 > 2
by Th10, A1, A2;
then consider p being Element of NAT such that
A3:
p is prime
and
A4:
p divides m1
by NAT_1:13, INT_2:31;
A5:
p > 1
by A3, INT_2:def 4;
reconsider p = p as non zero Element of NAT by A3, INT_2:def 4;
A6:
2 divides card (Im (FSG,x))
by Th8;
A7:
p > 2
then reconsider p2 = p - 2 as Nat by NAT_1:21;
reconsider p1 = p - 1 as Nat by NAT_1:20, A3, INT_2:def 4;
set T1 = p1 -tuples_on F;
set XFSG1 = { f where f is Element of p1 -tuples_on F : ( S1[f] & f . 1 = f . p1 ) } ;
set XFSG2 = { f where f is Element of p1 -tuples_on F : ( S1[f] & f . 1 <> f . p1 ) } ;
defpred S2[ object , object ] means for f being FinSequence st f = $1 holds
$2 = f | p1;
A10:
for x being object st x in F holds
H1(x) in bool F
consider IM being Function of F,(bool F) such that
A11:
for x being object st x in F holds
IM . x = H1(x)
from FUNCT_2:sch 2(A10);
A12:
for x being object st x in F holds
card (IM . x) = card (Im (FSG,x))
defpred S3[ FinSequence] means ( [($1 . p),($1 . 1)] in FSG & S1[$1] );
set T = p -tuples_on F;
set XT = { f where f is Element of p -tuples_on F : S3[f] } ;
set XFSG = { f where f is Element of (p2 + 1) -tuples_on F : ( f . 1 in F & ( for i being Nat st i in Seg p2 holds
f . (i + 1) in IM . (f . i) ) ) } ;
F c= F
;
then A14:
card { f where f is Element of (p2 + 1) -tuples_on F : ( f . 1 in F & ( for i being Nat st i in Seg p2 holds
f . (i + 1) in IM . (f . i) ) ) } = (card F) * ((card (Im (FSG,x))) |^ p2)
by A12, Th6;
then reconsider XFSG = { f where f is Element of (p2 + 1) -tuples_on F : ( f . 1 in F & ( for i being Nat st i in Seg p2 holds
f . (i + 1) in IM . (f . i) ) ) } as finite set ;
A15:
for f being Element of p1 -tuples_on F holds
( f in XFSG iff S1[f] )
A27:
{ f where f is Element of p1 -tuples_on F : ( S1[f] & f . 1 = f . p1 ) } c= XFSG
A28:
{ f where f is Element of p1 -tuples_on F : ( S1[f] & f . 1 <> f . p1 ) } c= XFSG
then reconsider XFSG1 = { f where f is Element of p1 -tuples_on F : ( S1[f] & f . 1 = f . p1 ) } , XFSG2 = { f where f is Element of p1 -tuples_on F : ( S1[f] & f . 1 <> f . p1 ) } as finite set by A27;
A29:
p > 1
by A3, INT_2:def 4;
then
not p divides m1 + 1
by A4, NEWTON:39;
then A30:
not p divides (card (Im (FSG,x))) |^ p2
by A3, NAT_3:5;
A31:
XFSG1 misses XFSG2
A33:
for x being object st x in { f where f is Element of p -tuples_on F : S3[f] } holds
ex y being object st
( y in XFSG & S2[x,y] )
proof
let x be
object ;
( x in { f where f is Element of p -tuples_on F : S3[f] } implies ex y being object st
( y in XFSG & S2[x,y] ) )
assume
x in { f where f is Element of p -tuples_on F : S3[f] }
;
ex y being object st
( y in XFSG & S2[x,y] )
then consider f being
Element of
p -tuples_on F such that A34:
x = f
and A35:
S3[
f]
;
set g =
f | p1;
A36:
len f = p1 + 1
by CARD_1:def 7;
then
p1 < len f
by NAT_1:13;
then A37:
len (f | p1) = p1
by FINSEQ_1:59;
then reconsider g =
f | p1 as
Element of
p1 -tuples_on F by FINSEQ_2:92;
take
g
;
( g in XFSG & S2[x,g] )
S1[
g]
proof
let i be
Nat;
( 1 <= i & i < len g implies [(g . i),(g . (i + 1))] in FSG )
assume that A38:
1
<= i
and A39:
i < len g
;
[(g . i),(g . (i + 1))] in FSG
i in dom g
by A38, A39, FINSEQ_3:25;
then A40:
f . i = g . i
by FUNCT_1:47;
i < len f
by A39, A36, NAT_1:13, A37;
then A41:
[(f . i),(f . (i + 1))] in FSG
by A38, A35;
( 1
< i + 1 &
i + 1
<= len g )
by A38, NAT_1:13, A39;
then
i + 1
in dom g
by FINSEQ_3:25;
hence
[(g . i),(g . (i + 1))] in FSG
by A40, FUNCT_1:47, A41;
verum
end;
hence
(
g in XFSG &
S2[
x,
g] )
by A15, A34;
verum
end;
consider FSGR being Function of { f where f is Element of p -tuples_on F : S3[f] } ,XFSG such that
A42:
for x being object st x in { f where f is Element of p -tuples_on F : S3[f] } holds
S2[x,FSGR . x]
from FUNCT_2:sch 1(A33);
reconsider pr = FSGR ~ as Relation ;
card (Im (FSG,x)) > 2
by Th10, A1, A2;
then
(card (Im (FSG,x))) |^ p2 > 0
by NEWTON:83;
then A43:
not XFSG is empty
by XREAL_1:129, A14;
then A44:
dom FSGR = { f where f is Element of p -tuples_on F : S3[f] }
by FUNCT_2:def 1;
A45:
XFSG c= XFSG1 \/ XFSG2
A49:
p = p1 + 1
;
then A50:
p1 >= 1
by A29, NAT_1:13;
A51:
for y being object
for f being Element of p1 -tuples_on F st S1[f] & [(f . p1),y] in FSG & [y,(f . 1)] in FSG holds
f ^ <*y*> in { f where f is Element of p -tuples_on F : S3[f] }
proof
let y be
object ;
for f being Element of p1 -tuples_on F st S1[f] & [(f . p1),y] in FSG & [y,(f . 1)] in FSG holds
f ^ <*y*> in { f where f is Element of p -tuples_on F : S3[f] } let f be
Element of
p1 -tuples_on F;
( S1[f] & [(f . p1),y] in FSG & [y,(f . 1)] in FSG implies f ^ <*y*> in { f where f is Element of p -tuples_on F : S3[f] } )
assume that A52:
S1[
f]
and A53:
[(f . p1),y] in FSG
and A54:
[y,(f . 1)] in FSG
;
f ^ <*y*> in { f where f is Element of p -tuples_on F : S3[f] }
set fy =
f ^ <*y*>;
y in F
by A53, RELAT_1:15;
then
<*y*> is
FinSequence of
F
by FINSEQ_1:74;
then A55:
f ^ <*y*> is
FinSequence of
F
by FINSEQ_1:75;
A56:
len (f ^ <*y*>) = p1 + 1
by CARD_1:def 7;
A57:
len f = p1
by CARD_1:def 7;
then A58:
(f ^ <*y*>) . p = y
by FINSEQ_1:42;
reconsider fy =
f ^ <*y*> as
Element of
p -tuples_on F by A55, A56, FINSEQ_2:92;
A59:
S1[
fy]
1
in dom f
by A50, A57, FINSEQ_3:25;
then
[(fy . p),(fy . 1)] in FSG
by FINSEQ_1:def 7, A58, A54;
hence
f ^ <*y*> in { f where f is Element of p -tuples_on F : S3[f] }
by A59;
verum
end;
A67:
for f being Element of p1 -tuples_on F st S1[f] & f . 1 = f . p1 holds
for y being object st y in Im (FSG,(f . 1)) holds
f ^ <*y*> in { f where f is Element of p -tuples_on F : S3[f] }
A71:
for x being object st x in XFSG1 holds
card (Im (pr,x)) = card (Im (FSG,x))
proof
let x be
object ;
( x in XFSG1 implies card (Im (pr,x)) = card (Im (FSG,x)) )
assume
x in XFSG1
;
card (Im (pr,x)) = card (Im (FSG,x))
then consider f being
Element of
p1 -tuples_on F such that A72:
f = x
and A73:
(
S1[
f] &
f . 1
= f . p1 )
;
deffunc H2(
object )
-> set =
f ^ <*$1*>;
A74:
len f = p1
by CARD_1:def 7;
A75:
for
y being
object st
y in Im (
FSG,
(f . 1)) holds
H2(
y)
in Im (
pr,
f)
proof
let y be
object ;
( y in Im (FSG,(f . 1)) implies H2(y) in Im (pr,f) )
assume A76:
y in Im (
FSG,
(f . 1))
;
H2(y) in Im (pr,f)
then A77:
H2(
y)
in { f where f is Element of p -tuples_on F : S3[f] }
by A67, A73;
then consider fy being
Element of
p -tuples_on F such that A78:
H2(
y)
= fy
and
S3[
fy]
;
reconsider yy =
<*y*> as
FinSequence of
F by A78, FINSEQ_1:36;
FSGR . H2(
y) =
(f ^ yy) | p1
by A76, A67, A73, A42
.=
f
by A74, FINSEQ_5:23
;
then
[fy,f] in FSGR
by A77, A78, A44, FUNCT_1:def 2;
then
[f,fy] in pr
by RELAT_1:def 7;
hence
H2(
y)
in Im (
pr,
f)
by A78, RELAT_1:169;
verum
end;
consider d being
Function of
(Im (FSG,(f . 1))),
(Im (pr,f)) such that A79:
for
y being
object st
y in Im (
FSG,
(f . 1)) holds
d . y = H2(
y)
from FUNCT_2:sch 2(A75);
A80:
d is
one-to-one
A83:
1
in dom f
by A74, A50, FINSEQ_3:25;
then
f . 1
in rng f
by FUNCT_1:def 3;
then A84:
card (Im (FSG,(f . 1))) = card (Im (FSG,x))
by A1, Th11, A2;
then
not
Im (
FSG,
(f . 1)) is
empty
by Th10, A1, A2;
then
ex
xx being
object st
xx in Im (
FSG,
(f . 1))
;
then
not
Im (
pr,
f) is
empty
by A75;
then A85:
dom d = Im (
FSG,
(f . 1))
by FUNCT_2:def 1;
Im (
pr,
f)
c= rng d
proof
let y be
object ;
TARSKI:def 3 ( not y in Im (pr,f) or y in rng d )
assume
y in Im (
pr,
f)
;
y in rng d
then
[f,y] in pr
by RELAT_1:169;
then A86:
[y,f] in FSGR
by RELAT_1:def 7;
then A87:
y in dom FSGR
by XTUPLE_0:def 12;
then consider g being
Element of
p -tuples_on F such that A88:
y = g
and A89:
S3[
g]
by A44;
A90:
len g = p1 + 1
by CARD_1:def 7;
f = FSGR . y
by A87, A86, FUNCT_1:def 2;
then
g | p1 = f
by A87, A42, A88;
then A91:
g = f ^ <*(g . p)*>
by A90, FINSEQ_3:55;
then
g . 1
= f . 1
by A83, FINSEQ_1:def 7;
then A92:
[(f . 1),(g . p)] in FSG
by A89, Lm3;
then
g . p in dom d
by RELAT_1:169, A85;
then
d . (g . p) in rng d
by FUNCT_1:def 3;
hence
y in rng d
by A92, RELAT_1:169, A91, A79, A88;
verum
end;
then
Im (
pr,
f)
= rng d
;
hence
card (Im (pr,x)) = card (Im (FSG,x))
by A85, A80, WELLORD2:def 4, A84, CARD_1:5, A72;
verum
end;
XFSG1 \/ XFSG2 c= XFSG
by A27, XBOOLE_1:8, A28;
then A93:
XFSG = XFSG1 \/ XFSG2
by A45;
then
card XFSG = (card XFSG1) + (card XFSG2)
by A31, CARD_2:40;
then A94:
(1 + ((card (Im (FSG,x))) * m1)) * ((card (Im (FSG,x))) |^ p2) = (card XFSG1) + (card XFSG2)
by A14, A1, A2, Th12;
A95:
for f being Element of p1 -tuples_on F st S1[f] & f . 1 <> f . p1 holds
ex y being object st
( y in F & f ^ <*y*> in { f where f is Element of p -tuples_on F : S3[f] } )
proof
let f be
Element of
p1 -tuples_on F;
( S1[f] & f . 1 <> f . p1 implies ex y being object st
( y in F & f ^ <*y*> in { f where f is Element of p -tuples_on F : S3[f] } ) )
assume that A96:
S1[
f]
and A97:
f . 1
<> f . p1
;
ex y being object st
( y in F & f ^ <*y*> in { f where f is Element of p -tuples_on F : S3[f] } )
A98:
len f = p1
by CARD_1:def 7;
then
p1 in dom f
by A50, FINSEQ_3:25;
then A99:
f . p1 in rng f
by FUNCT_1:def 3;
1
in dom f
by A98, A50, FINSEQ_3:25;
then
f . 1
in rng f
by FUNCT_1:def 3;
then consider w being
object such that A100:
{w} = (Im (FSG,(f . p1))) /\ (Coim (FSG,(f . 1)))
by A99, A97, Def3;
take
w
;
( w in F & f ^ <*w*> in { f where f is Element of p -tuples_on F : S3[f] } )
A101:
w in {w}
by TARSKI:def 1;
Coim (
FSG,
(f . 1))
= Im (
FSG,
(f . 1))
by Th2;
then
w in Im (
FSG,
(f . 1))
by A101, A100, XBOOLE_0:def 4;
then
[(f . 1),w] in FSG
by RELAT_1:169;
then A102:
[w,(f . 1)] in FSG
by Lm3;
w in Im (
FSG,
(f . p1))
by A101, A100, XBOOLE_0:def 4;
then
[(f . p1),w] in FSG
by RELAT_1:169;
hence
(
w in F &
f ^ <*w*> in { f where f is Element of p -tuples_on F : S3[f] } )
by A102, A51, A96, RELAT_1:15;
verum
end;
A103:
for x being object st x in XFSG2 holds
card (Im ((pr | XFSG2),x)) = 1
proof
let x be
object ;
( x in XFSG2 implies card (Im ((pr | XFSG2),x)) = 1 )
assume A104:
x in XFSG2
;
card (Im ((pr | XFSG2),x)) = 1
consider f being
Element of
p1 -tuples_on F such that A105:
x = f
and A106:
S1[
f]
and A107:
f . 1
<> f . p1
by A104;
consider y being
object such that
y in F
and A109:
f ^ <*y*> in { f where f is Element of p -tuples_on F : S3[f] }
by A95, A106, A107;
A111:
len f = p1
by CARD_1:def 7;
A112:
Im (
(pr | XFSG2),
f)
c= {(f ^ <*y*>)}
proof
let z be
object ;
TARSKI:def 3 ( not z in Im ((pr | XFSG2),f) or z in {(f ^ <*y*>)} )
consider w being
Element of
p -tuples_on F such that A113:
w = f ^ <*y*>
and A114:
S3[
w]
by A109;
A115:
w . p = y
by A113, A111, FINSEQ_1:42;
A116:
p1 in dom f
by A50, A111, FINSEQ_3:25;
then A117:
w . p1 = f . p1
by A113, FINSEQ_1:def 7;
A118:
1
in dom f
by A50, A111, FINSEQ_3:25;
then A119:
w . 1
= f . 1
by A113, FINSEQ_1:def 7;
assume
z in Im (
(pr | XFSG2),
f)
;
z in {(f ^ <*y*>)}
then
[f,z] in pr | XFSG2
by RELAT_1:169;
then
[f,z] in pr
by RELAT_1:def 11;
then A120:
[z,f] in FSGR
by RELAT_1:def 7;
then A121:
z in dom FSGR
by XTUPLE_0:def 12;
then
z in { f where f is Element of p -tuples_on F : S3[f] }
;
then consider g being
Element of
p -tuples_on F such that A122:
g = z
and A123:
S3[
g]
;
A124:
p1 < p
by A49, NAT_1:13;
f = FSGR . z
by A121, FUNCT_1:def 2, A120;
then A125:
f = g | p1
by A121, A42, A122;
then A126:
g . 1
= f . 1
by A118, FUNCT_1:47;
len w = p
by CARD_1:def 7;
then A127:
[(w . p1),(w . p)] in FSG
by A49, A29, NAT_1:13, A124, A114;
A128:
len g = p
by CARD_1:def 7;
then A129:
g = f ^ <*(g . p)*>
by A125, FINSEQ_3:55;
A130:
g . p1 = f . p1
by A116, A125, FUNCT_1:47;
[(g . p1),(g . p)] in FSG
by A49, A29, NAT_1:13, A124, A123, A128;
then
g . p = w . p
by A119, A126, A117, A130, A123, A114, A107, A127, Lm5;
hence
z in {(f ^ <*y*>)}
by A129, A115, A122, TARSKI:def 1;
verum
end;
FSGR . (f ^ <*y*>) =
(f ^ <*y*>) | p1
by A42, A109
.=
f
by FINSEQ_5:23, A111
;
then
[(f ^ <*y*>),f] in FSGR
by FUNCT_1:def 2, A44, A109;
then
[f,(f ^ <*y*>)] in pr
by RELAT_1:def 7;
then
[f,(f ^ <*y*>)] in pr | XFSG2
by A105, A104, RELAT_1:def 11;
then
f ^ <*y*> in Im (
(pr | XFSG2),
f)
by RELAT_1:169;
then
Im (
(pr | XFSG2),
f)
= {(f ^ <*y*>)}
by A112, ZFMISC_1:33;
hence
card (Im ((pr | XFSG2),x)) = 1
by A105, CARD_1:30;
verum
end;
(dom (pr | XFSG2)) \ XFSG2 = {}
by RELAT_1:58, XBOOLE_1:37;
then
card ((pr | XFSG2) | ((dom (pr | XFSG2)) \ XFSG2)) = 0
;
then A131: card (pr | XFSG2) =
0 +` (1 *` (card XFSG2))
by A103, SIMPLEX1:1
.=
1 *` (card XFSG2)
by CARD_2:18
.=
card XFSG2
by CARD_2:21
;
XFSG c= rng FSGR
proof
let xp be
object ;
TARSKI:def 3 ( not xp in XFSG or xp in rng FSGR )
assume A132:
xp in XFSG
;
xp in rng FSGR
per cases
( xp in XFSG1 or xp in XFSG2 )
by A132, A45, XBOOLE_0:def 3;
suppose
xp in XFSG1
;
xp in rng FSGRthen consider f being
Element of
p1 -tuples_on F such that A133:
xp = f
and A134:
(
S1[
f] &
f . 1
= f . p1 )
;
len f = p1
by CARD_1:def 7;
then
1
in dom f
by A50, FINSEQ_3:25;
then
f . 1
in rng f
by FUNCT_1:def 3;
then
card (Im (FSG,(f . 1))) = card (Im (FSG,x))
by A1, Th11, A2;
then
not
Im (
FSG,
(f . 1)) is
empty
by Th10, A1, A2;
then consider y being
object such that A135:
y in Im (
FSG,
(f . 1))
;
set fy =
y;
set fy =
f ^ <*y*>;
f ^ <*y*> in { f where f is Element of p -tuples_on F : S3[f] }
by A67, A134, A135;
then A136:
FSGR . (f ^ <*y*>) in rng FSGR
by A44, FUNCT_1:def 3;
[(f . 1),y] in FSG
by A135, RELAT_1:169;
then
y in F
by RELAT_1:15;
then
<*y*> is
FinSequence of
F
by FINSEQ_1:74;
then A138:
(
len (f ^ <*y*>) = p1 + 1 &
f ^ <*y*> is
FinSequence of
F )
by CARD_1:def 7, FINSEQ_1:75;
A139:
len f = p1
by CARD_1:def 7;
FSGR . (f ^ <*y*>) = (f ^ <*y*>) | p1
by A42, A67, A134, A135;
hence
xp in rng FSGR
by A139, FINSEQ_5:23, A133, A136;
verumreconsider fy =
f ^ <*y*> as
Element of
p -tuples_on F by A138, FINSEQ_2:92;
end; end;
end;
then
XFSG = rng FSGR
;
then
dom pr = XFSG
by RELAT_1:20;
then
(dom pr) \ XFSG1 = XFSG2
by XBOOLE_1:88, A93, A31;
then A146: card pr =
(card XFSG2) +` ((card (Im (FSG,x))) *` (card XFSG1))
by A131, A71, SIMPLEX1:1
.=
(card XFSG2) +` ((card (Im (FSG,x))) * (card XFSG1))
by Lm1
.=
(card XFSG2) + ((card (Im (FSG,x))) * (card XFSG1))
by Lm1
;
A147:
for f1, f2 being FinSequence of F st f1 ^ f2 is p -element & S3[f1 ^ f2] holds
S3[f2 ^ f1]
proof
let f1,
f2 be
FinSequence of
F;
( f1 ^ f2 is p -element & S3[f1 ^ f2] implies S3[f2 ^ f1] )
assume that A148:
f1 ^ f2 is
p -element
and A149:
S3[
f1 ^ f2]
;
S3[f2 ^ f1]
set f12 =
f1 ^ f2;
set f21 =
f2 ^ f1;
set L1 =
len f1;
set L2 =
len f2;
A150:
len (f1 ^ f2) = p
by CARD_1:def 7, A148;
A151:
len (f2 ^ f1) = (len f2) + (len f1)
by FINSEQ_1:22;
A152:
len (f1 ^ f2) = (len f1) + (len f2)
by FINSEQ_1:22;
per cases
( f1 = {} or f2 = {} or ( f1 <> {} & f2 <> {} ) )
;
suppose A153:
(
f1 <> {} &
f2 <> {} )
;
S3[f2 ^ f1]then
len f2 >= 1
by FINSEQ_1:20;
then A154:
1
in dom f2
by FINSEQ_3:25;
then A155:
(f1 ^ f2) . ((len f1) + 1) = f2 . 1
by FINSEQ_1:def 7;
A156:
(len f1) + 1
<= p
by A153, FINSEQ_1:20, A150, A152, XREAL_1:6;
A157:
len f1 >= 1
by A153, FINSEQ_1:20;
then A158:
1
in dom f1
by FINSEQ_3:25;
A159:
len f1 in dom f1
by A157, FINSEQ_3:25;
then A160:
(f2 ^ f1) . p = f1 . (len f1)
by A150, A152, FINSEQ_1:def 7;
(f1 ^ f2) . (len f1) = f1 . (len f1)
by A159, FINSEQ_1:def 7;
then
[(f1 . (len f1)),(f2 . 1)] in FSG
by A156, NAT_1:13, A149, A157, A155, A150;
hence
[((f2 ^ f1) . p),((f2 ^ f1) . 1)] in FSG
by A160, A154, FINSEQ_1:def 7;
S1[f2 ^ f1]let i be
Nat;
( 1 <= i & i < len (f2 ^ f1) implies [((f2 ^ f1) . i),((f2 ^ f1) . (i + 1))] in FSG )assume that A161:
1
<= i
and A162:
i < len (f2 ^ f1)
;
[((f2 ^ f1) . i),((f2 ^ f1) . (i + 1))] in FSGA163:
i in dom (f2 ^ f1)
by A161, A162, FINSEQ_3:25;
per cases
( i in dom f2 or ex n being Nat st
( n in dom f1 & i = (len f2) + n ) )
by A163, FINSEQ_1:25;
suppose A164:
i in dom f2
;
[((f2 ^ f1) . i),((f2 ^ f1) . (i + 1))] in FSGthen A165:
i <= len f2
by FINSEQ_3:25;
A166:
(f2 ^ f1) . i = f2 . i
by A164, FINSEQ_1:def 7;
per cases
( i = len f2 or i <> len f2 )
;
suppose A167:
i = len f2
;
[((f2 ^ f1) . i),((f2 ^ f1) . (i + 1))] in FSGA168:
f1 . 1
= (f1 ^ f2) . 1
by A158, FINSEQ_1:def 7;
f2 . i = (f1 ^ f2) . p
by A167, A150, A152, A164, FINSEQ_1:def 7;
hence
[((f2 ^ f1) . i),((f2 ^ f1) . (i + 1))] in FSG
by A168, A167, A158, FINSEQ_1:def 7, A149, A166;
verum end; suppose A169:
i <> len f2
;
[((f2 ^ f1) . i),((f2 ^ f1) . (i + 1))] in FSGA170:
1
+ 0 <= (len f1) + i
by XREAL_1:7, A157;
A171:
i < len f2
by A169, A165, XXREAL_0:1;
then
(len f1) + i < p
by A150, A152, XREAL_1:6;
then A172:
[((f1 ^ f2) . ((len f1) + i)),((f1 ^ f2) . (((len f1) + i) + 1))] in FSG
by A170, A149, A150;
A173:
(f1 ^ f2) . ((len f1) + i) = f2 . i
by A164, FINSEQ_1:def 7;
i + 1
<= len f2
by A171, NAT_1:13;
then A174:
i + 1
in dom f2
by NAT_1:11, FINSEQ_3:25;
then
(f1 ^ f2) . ((len f1) + (i + 1)) = f2 . (i + 1)
by FINSEQ_1:def 7;
hence
[((f2 ^ f1) . i),((f2 ^ f1) . (i + 1))] in FSG
by A174, FINSEQ_1:def 7, A172, A173, A166;
verum end; end; end; suppose
ex
n being
Nat st
(
n in dom f1 &
i = (len f2) + n )
;
[((f2 ^ f1) . i),((f2 ^ f1) . (i + 1))] in FSGthen consider n being
Nat such that A175:
n in dom f1
and A176:
i = (len f2) + n
;
A177:
(
(f2 ^ f1) . i = f1 . n &
(f1 ^ f2) . n = f1 . n )
by A175, A176, FINSEQ_1:def 7;
A178:
1
<= n
by A175, FINSEQ_3:25;
A179:
n < len f1
by A176, A162, A151, XREAL_1:6;
then A180:
n + 0 < (len f1) + (len f2)
by XREAL_1:8;
n + 1
<= len f1
by A179, NAT_1:13;
then A181:
n + 1
in dom f1
by NAT_1:11, FINSEQ_3:25;
i + 1
= (len f2) + (n + 1)
by A176;
then A182:
(f2 ^ f1) . (i + 1) = f1 . (n + 1)
by A181, FINSEQ_1:def 7;
(f1 ^ f2) . (n + 1) = f1 . (n + 1)
by A181, FINSEQ_1:def 7;
hence
[((f2 ^ f1) . i),((f2 ^ f1) . (i + 1))] in FSG
by A178, A180, A149, A152, A177, A182;
verum end; end; end; end;
end;
A183:
for f1 being Element of p -tuples_on F st S3[f1] holds
for i being Nat st i < p & f1 = (f1 /^ i) ^ (f1 | i) holds
i = 0
proof
let f1 be
Element of
p -tuples_on F;
( S3[f1] implies for i being Nat st i < p & f1 = (f1 /^ i) ^ (f1 | i) holds
i = 0 )
assume A184:
S3[
f1]
;
for i being Nat st i < p & f1 = (f1 /^ i) ^ (f1 | i) holds
i = 0
A185:
len f1 = p
by CARD_1:def 7;
then
2
in dom f1
by A7, FINSEQ_3:25;
then A186:
f1 . 2
in rng f1
by FUNCT_1:def 3;
let i be
Nat;
( i < p & f1 = (f1 /^ i) ^ (f1 | i) implies i = 0 )
assume A187:
(
i < p &
f1 = (f1 /^ i) ^ (f1 | i) &
i <> 0 )
;
contradiction
rng f1 c= {(f1 . 1)}
by A187, A185, A3, Th7;
then A188:
f1 . 2
= f1 . 1
by A186, TARSKI:def 1;
[(f1 . 1),(f1 . (1 + 1))] in FSG
by A3, INT_2:def 4, A184, A185;
hence
contradiction
by A188, Lm2;
verum
end;
consider C being Cardinal such that
A189:
p *` C = card { f where f is Element of p -tuples_on F : S3[f] }
from FRIENDS1:sch 1(A147, A183);
A190: card pr =
card FSGR
by Th1
.=
card (dom FSGR)
by CARD_1:62
.=
card { f where f is Element of p -tuples_on F : S3[f] }
by A43, FUNCT_2:def 1
;
then
C is finite
by A146, A189;
then reconsider C = C as Nat ;
p * C = (card XFSG2) + ((card (Im (FSG,x))) * (card XFSG1))
by A189, Lm1, A146, A190;
then A191:
p divides ((1 + ((card (Im (FSG,x))) * m1)) * ((card (Im (FSG,x))) |^ p2)) + (((card (Im (FSG,x))) - 1) * (card XFSG1))
by A94, INT_1:def 3;
not p divides ((card (Im (FSG,x))) * m1) + 1
by A4, INT_2:2, NEWTON:39, A29;
then A192:
not p divides (1 + ((card (Im (FSG,x))) * m1)) * ((card (Im (FSG,x))) |^ p2)
by A30, A3, INT_5:7;
p divides m1 * (card XFSG1)
by A4, INT_2:2;
hence
contradiction
by A192, INT_2:1, A191; verum