let FSG be Friendship_Graph; :: thesis: ( not FSG is empty implies FSG is with_universal_friend )
set F = field FSG;
defpred S₁[ FinSequence] means for i being Nat st 1 <= i & i < len $1 holds
[($1 . i),($1 . (i + 1))] in FSG;
deffunc H₁( object ) -> set = Im (FSG,$1);
assume A1: ( not FSG is empty & FSG is without_universal_friend ) ; :: thesis: 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

proof

A8: m1 + 1 = card (Im (FSG,x)) ;
assume A9: p <= 2 ; :: thesis: contradiction
p >= 1 + 1 by A5, NAT_1:13;
then 2 divides m1 by A9, XXREAL_0:1, A4;
then 2 divides 1 by A8, INT_2:1, A6;
hence contradiction by INT_2:13; :: thesis: verum

end;

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 : ( S₁[f] & f . 1 = f . p1 ) } ;
set XFSG2 = { f where f is Element of p1 -tuples_on F : ( S₁[f] & f . 1 <> f . p1 ) } ;
defpred S₂[ object , object ] means for f being FinSequence st f = $1 holds
$2 = f | p1;
A10: for x being object st x in F holds
H₁(x) in bool F

proof

let x be object ; :: thesis: ( x in F implies H₁(x) in bool F )
assume x in F ; :: thesis: H₁(x) in bool F
H₁(x) c= F

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in H₁(x) or y in F )
assume y in H₁(x) ; :: thesis: y in F
then [x,y] in FSG by RELAT_1:169;
hence y in F by RELAT_1:15; :: thesis: verum

end;

hence H₁(x) in bool F ; :: thesis: verum

end;

consider IM being Function of F,(bool F) such that
A11: for x being object st x in F holds
IM . x = H₁(x) from FUNCT_2:sch 2(A10);
A12: for x being object st x in F holds
card (IM . x) = card (Im (FSG,x))

proof

let y be object ; :: thesis: ( y in F implies card (IM . y) = card (Im (FSG,x)) )
assume A13: y in F ; :: thesis: card (IM . y) = card (Im (FSG,x))
hence card (IM . y) = card H₁(y) by A11
.= card (Im (FSG,x)) by A2, Th11, A1, A13 ;
:: thesis: verum

end;

defpred S₃[ FinSequence] means ( [($1 . p),($1 . 1)] in FSG & S₁[$1] );
set T = p -tuples_on F;
set XT = { f where f is Element of p -tuples_on F : S₃[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 S₁[f] )

proof

let f be Element of p1 -tuples_on F; :: thesis: ( f in XFSG iff S₁[f] )
A16: len f = p2 + 1 by CARD_1:def 7;

hereby :: thesis: ( S₁[f] implies f in XFSG )

assume f in XFSG ; :: thesis: S₁[f]
then A17: ex g being Element of p1 -tuples_on F st
( f = g & g . 1 in F & ( for i being Nat st i in Seg p2 holds
g . (i + 1) in IM . (g . i) ) ) ;
thus S₁[f] :: thesis: verum

proof

let i be Nat; :: thesis: ( 1 <= i & i < len f implies [(f . i),(f . (i + 1))] in FSG )
assume that
A18: 1 <= i and
A19: i < len f ; :: thesis: [(f . i),(f . (i + 1))] in FSG
i in dom f by A18, A19, FINSEQ_3:25;
then f . i in rng f by FUNCT_1:def 3;
then A20: H₁(f . i) = IM . (f . i) by A11;
i <= p2 by A19, A16, NAT_1:13;
then i in Seg p2 by A18;
hence [(f . i),(f . (i + 1))] in FSG by A17, A20, RELAT_1:169; :: thesis: verum

end;

end;

assume A21: S₁[f] ; :: thesis: f in XFSG
A22: for i being Nat st i in Seg p2 holds
f . (i + 1) in IM . (f . i)

proof

let i be Nat; :: thesis: ( i in Seg p2 implies f . (i + 1) in IM . (f . i) )
assume A23: i in Seg p2 ; :: thesis: f . (i + 1) in IM . (f . i)
then A24: 1 <= i by FINSEQ_1:1;
i <= p2 by A23, FINSEQ_1:1;
then A25: i < p2 + 1 by NAT_1:13;
then i in dom f by A24, A16, FINSEQ_3:25;
then A26: f . i in rng f by FUNCT_1:def 3;
[(f . i),(f . (i + 1))] in FSG by A24, A25, A21, A16;
then f . (i + 1) in H₁(f . i) by RELAT_1:169;
hence f . (i + 1) in IM . (f . i) by A26, A11; :: thesis: verum

end;

1 <= len f by A16, NAT_1:11;
then 1 in dom f by FINSEQ_3:25;
then f . 1 in rng f by FUNCT_1:def 3;
hence f in XFSG by A22; :: thesis: verum

end;

A27: { f where f is Element of p1 -tuples_on F : ( S₁[f] & f . 1 = f . p1 ) } c= XFSG

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Element of p1 -tuples_on F : ( S₁[f] & f . 1 = f . p1 ) } or x in XFSG )
assume x in { f where f is Element of p1 -tuples_on F : ( S₁[f] & f . 1 = f . p1 ) } ; :: thesis: x in XFSG
then ex f being Element of p1 -tuples_on F st
( x = f & S₁[f] & f . 1 = f . p1 ) ;
hence x in XFSG by A15; :: thesis: verum

end;

A28: { f where f is Element of p1 -tuples_on F : ( S₁[f] & f . 1 <> f . p1 ) } c= XFSG

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Element of p1 -tuples_on F : ( S₁[f] & f . 1 <> f . p1 ) } or x in XFSG )
assume x in { f where f is Element of p1 -tuples_on F : ( S₁[f] & f . 1 <> f . p1 ) } ; :: thesis: x in XFSG
then ex f being Element of p1 -tuples_on F st
( x = f & S₁[f] & f . 1 <> f . p1 ) ;
hence x in XFSG by A15; :: thesis: verum

end;

then reconsider XFSG1 = { f where f is Element of p1 -tuples_on F : ( S₁[f] & f . 1 = f . p1 ) } , XFSG2 = { f where f is Element of p1 -tuples_on F : ( S₁[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

proof

assume XFSG1 meets XFSG2 ; :: thesis: contradiction
then consider x being object such that
A32: ( x in XFSG1 & x in XFSG2 ) by XBOOLE_0:3;
( ex f being Element of p1 -tuples_on F st
( x = f & S₁[f] & f . 1 = f . p1 ) & ex f being Element of p1 -tuples_on F st
( x = f & S₁[f] & f . 1 <> f . p1 ) ) by A32;
hence contradiction ; :: thesis: verum

end;

A33: for x being object st x in { f where f is Element of p -tuples_on F : S₃[f] } holds
ex y being object st
( y in XFSG & S₂[x,y] )

proof

let x be object ; :: thesis: ( x in { f where f is Element of p -tuples_on F : S₃[f] } implies ex y being object st
( y in XFSG & S₂[x,y] ) )
assume x in { f where f is Element of p -tuples_on F : S₃[f] } ; :: thesis: ex y being object st
( y in XFSG & S₂[x,y] )
then consider f being Element of p -tuples_on F such that
A34: x = f and
A35: S₃[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 ; :: thesis: ( g in XFSG & S₂[x,g] )
S₁[g]

proof

let i be Nat; :: thesis: ( 1 <= i & i < len g implies [(g . i),(g . (i + 1))] in FSG )
assume that
A38: 1 <= i and
A39: i < len g ; :: thesis: [(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; :: thesis: verum

end;

hence ( g in XFSG & S₂[x,g] ) by A15, A34; :: thesis: verum

end;

consider FSGR being Function of { f where f is Element of p -tuples_on F : S₃[f] } ,XFSG such that
A42: for x being object st x in { f where f is Element of p -tuples_on F : S₃[f] } holds
S₂[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 : S₃[f] } by FUNCT_2:def 1;
A45: XFSG c= XFSG1 \/ XFSG2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in XFSG or x in XFSG1 \/ XFSG2 )
assume A46: x in XFSG ; :: thesis: x in XFSG1 \/ XFSG2
then consider f being Element of (p2 + 1) -tuples_on F such that
A47: x = f and
( f . 1 in F & ( for i being Nat st i in Seg p2 holds
f . (i + 1) in IM . (f . i) ) ) ;
A48: ( f . 1 = f . p1 or f . 1 <> f . p1 ) ;
S₁[f] by A15, A46, A47;
then ( f in XFSG1 or f in XFSG2 ) by A48;
hence x in XFSG1 \/ XFSG2 by XBOOLE_0:def 3, A47; :: thesis: verum

end;

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 S₁[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 : S₃[f] }

proof

let y be object ; :: thesis: for f being Element of p1 -tuples_on F st S₁[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 : S₃[f] }
let f be Element of p1 -tuples_on F; :: thesis: ( S₁[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 : S₃[f] } )
assume that
A52: S₁[f] and
A53: [(f . p1),y] in FSG and
A54: [y,(f . 1)] in FSG ; :: thesis: f ^ <*y*> in { f where f is Element of p -tuples_on F : S₃[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: S₁[fy]

proof

let i be Nat; :: thesis: ( 1 <= i & i < len fy implies [(fy . i),(fy . (i + 1))] in FSG )
assume that
A60: 1 <= i and
A61: i < len fy ; :: thesis: [(fy . i),(fy . (i + 1))] in FSG
A62: i <= p1 by A61, A56, NAT_1:13;
then A63: i in dom f by A60, A57, FINSEQ_3:25;
then A64: f . i = fy . i by FINSEQ_1:def 7;

per cases ( i = p1 or i < p1 ) by A62, XXREAL_0:1;

suppose i = p1 ; :: thesis: [(fy . i),(fy . (i + 1))] in FSG

hence [(fy . i),(fy . (i + 1))] in FSG by A58, A63, FINSEQ_1:def 7, A53; :: thesis: verum

end;

suppose A65: i < p1 ; :: thesis: [(fy . i),(fy . (i + 1))] in FSG

then i + 1 <= p1 by NAT_1:13;
then A66: i + 1 in dom f by NAT_1:11, A57, FINSEQ_3:25;
[(f . i),(f . (i + 1))] in FSG by A65, A57, A52, A60;
hence [(fy . i),(fy . (i + 1))] in FSG by A66, FINSEQ_1:def 7, A64; :: thesis: verum

end;

end;

end;

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 : S₃[f] } by A59; :: thesis: verum

end;

A67: for f being Element of p1 -tuples_on F st S₁[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 : S₃[f] }

proof

let f be Element of p1 -tuples_on F; :: thesis: ( S₁[f] & f . 1 = f . p1 implies 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 : S₃[f] } )
assume A68: ( S₁[f] & f . 1 = f . p1 ) ; :: thesis: 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 : S₃[f] }
let y be object ; :: thesis: ( y in Im (FSG,(f . 1)) implies f ^ <*y*> in { f where f is Element of p -tuples_on F : S₃[f] } )
assume A69: y in Im (FSG,(f . 1)) ; :: thesis: f ^ <*y*> in { f where f is Element of p -tuples_on F : S₃[f] }
A70: [(f . 1),y] in FSG by RELAT_1:169, A69;
then [y,(f . 1)] in FSG by Lm3;
hence f ^ <*y*> in { f where f is Element of p -tuples_on F : S₃[f] } by A68, A70, A51; :: thesis: verum

end;

A71: for x being object st x in XFSG1 holds
card (Im (pr,x)) = card (Im (FSG,x))

proof

let x be object ; :: thesis: ( x in XFSG1 implies card (Im (pr,x)) = card (Im (FSG,x)) )
assume x in XFSG1 ; :: thesis: 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: ( S₁[f] & f . 1 = f . p1 ) ;
deffunc H₂( 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
H₂(y) in Im (pr,f)

proof

let y be object ; :: thesis: ( y in Im (FSG,(f . 1)) implies H₂(y) in Im (pr,f) )
assume A76: y in Im (FSG,(f . 1)) ; :: thesis: H₂(y) in Im (pr,f)
then A77: H₂(y) in { f where f is Element of p -tuples_on F : S₃[f] } by A67, A73;
then consider fy being Element of p -tuples_on F such that
A78: H₂(y) = fy and
S₃[fy] ;
reconsider yy = <*y*> as FinSequence of F by A78, FINSEQ_1:36;
FSGR . H₂(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 H₂(y) in Im (pr,f) by A78, RELAT_1:169; :: thesis: 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 = H₂(y) from FUNCT_2:sch 2(A75);
A80: d is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom d or not x2 in dom d or not d . x1 = d . x2 or x1 = x2 )
assume that
A81: x1 in dom d and
A82: ( x2 in dom d & d . x1 = d . x2 ) ; :: thesis: x1 = x2
d . x1 = H₂(x1) by A81, A79;
then H₂(x1) = H₂(x2) by A82, A79;
hence x1 = x2 by FINSEQ_2:17; :: thesis: verum

end;

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 ; :: according to TARSKI:def 3 :: thesis: ( not y in Im (pr,f) or y in rng d )
assume y in Im (pr,f) ; :: thesis: 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: S₃[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; :: thesis: 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; :: thesis: 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 S₁[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 : S₃[f] } )

proof

let f be Element of p1 -tuples_on F; :: thesis: ( S₁[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 : S₃[f] } ) )
assume that
A96: S₁[f] and
A97: f . 1 <> f . p1 ; :: thesis: ex y being object st
( y in F & f ^ <*y*> in { f where f is Element of p -tuples_on F : S₃[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 ; :: thesis: ( w in F & f ^ <*w*> in { f where f is Element of p -tuples_on F : S₃[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 : S₃[f] } ) by A102, A51, A96, RELAT_1:15; :: thesis: verum

end;

A103: for x being object st x in XFSG2 holds
card (Im ((pr | XFSG2),x)) = 1

proof

let x be object ; :: thesis: ( x in XFSG2 implies card (Im ((pr | XFSG2),x)) = 1 )
assume A104: x in XFSG2 ; :: thesis: card (Im ((pr | XFSG2),x)) = 1
consider f being Element of p1 -tuples_on F such that
A105: x = f and
A106: S₁[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 : S₃[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 ; :: according to TARSKI:def 3 :: thesis: ( 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: S₃[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) ; :: thesis: 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 : S₃[f] } ;
then consider g being Element of p -tuples_on F such that
A122: g = z and
A123: S₃[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; :: thesis: 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; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not xp in XFSG or xp in rng FSGR )
assume A132: xp in XFSG ; :: thesis: xp in rng FSGR

per cases ( xp in XFSG1 or xp in XFSG2 ) by A132, A45, XBOOLE_0:def 3;

suppose xp in XFSG1 ; :: thesis: xp in rng FSGR

then consider f being Element of p1 -tuples_on F such that
A133: xp = f and
A134: ( S₁[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 : S₃[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; :: thesis: verum
reconsider fy = f ^ <*y*> as Element of p -tuples_on F by A138, FINSEQ_2:92;

end;

suppose xp in XFSG2 ; :: thesis: xp in rng FSGR

then consider f being Element of p1 -tuples_on F such that
A140: xp = f and
A141: ( S₁[f] & f . 1 <> f . p1 ) ;
consider y being object such that
A142: y in F and
A143: f ^ <*y*> in { f where f is Element of p -tuples_on F : S₃[f] } by A141, A95;
set fy = f ^ <*y*>;
A144: ( FSGR . (f ^ <*y*>) = (f ^ <*y*>) | p1 & FSGR . (f ^ <*y*>) in rng FSGR ) by A42, A143, A44, FUNCT_1:def 3;
<*y*> is FinSequence of F by A142, FINSEQ_1:74;
then ( len (f ^ <*y*>) = p1 + 1 & f ^ <*y*> is FinSequence of F ) by CARD_1:def 7, FINSEQ_1:75;
then reconsider fy = f ^ <*y*> as Element of p -tuples_on F by FINSEQ_2:92;
len f = p1 by CARD_1:def 7;
hence xp in rng FSGR by FINSEQ_5:23, A140, A144; :: thesis: verum

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 & S₃[f1 ^ f2] holds
S₃[f2 ^ f1]

proof

let f1, f2 be FinSequence of F; :: thesis: ( f1 ^ f2 is p -element & S₃[f1 ^ f2] implies S₃[f2 ^ f1] )
assume that
A148: f1 ^ f2 is p -element and
A149: S₃[f1 ^ f2] ; :: thesis: S₃[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 ( f1 = {} or f2 = {} ) ; :: thesis: S₃[f2 ^ f1]

then ( ( f1 ^ f2 = f2 & f2 ^ f1 = f2 ) or ( f1 ^ f2 = f1 & f2 ^ f1 = f1 ) ) by FINSEQ_1:34;
hence S₃[f2 ^ f1] by A149; :: thesis: verum

end;

suppose A153: ( f1 <> {} & f2 <> {} ) ; :: thesis: S₃[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; :: thesis: S₁[f2 ^ f1]
let i be Nat; :: thesis: ( 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) ; :: thesis: [((f2 ^ f1) . i),((f2 ^ f1) . (i + 1))] in FSG
A163: 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 ; :: thesis: [((f2 ^ f1) . i),((f2 ^ f1) . (i + 1))] in FSG

then 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 ; :: thesis: [((f2 ^ f1) . i),((f2 ^ f1) . (i + 1))] in FSG

A168: 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; :: thesis: verum

end;

suppose A169: i <> len f2 ; :: thesis: [((f2 ^ f1) . i),((f2 ^ f1) . (i + 1))] in FSG

A170: 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; :: thesis: verum

end;

end;

end;

suppose ex n being Nat st
( n in dom f1 & i = (len f2) + n ) ; :: thesis: [((f2 ^ f1) . i),((f2 ^ f1) . (i + 1))] in FSG

then 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; :: thesis: verum

end;

end;

end;

end;

end;

A183: for f1 being Element of p -tuples_on F st S₃[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; :: thesis: ( S₃[f1] implies for i being Nat st i < p & f1 = (f1 /^ i) ^ (f1 | i) holds
i = 0 )
assume A184: S₃[f1] ; :: thesis: 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; :: thesis: ( i < p & f1 = (f1 /^ i) ^ (f1 | i) implies i = 0 )
assume A187: ( i < p & f1 = (f1 /^ i) ^ (f1 | i) & i <> 0 ) ; :: thesis: 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; :: thesis: verum

end;

consider C being Cardinal such that
A189: p *` C = card { f where f is Element of p -tuples_on F : S₃[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 : S₃[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; :: thesis: verum