let x be object ; :: thesis: for FSG being Friendship_Graph holds 2 divides card (Im (FSG,x))
let FSG be Friendship_Graph; :: thesis: 2 divides card (Im (FSG,x))
set I = Im (FSG,x);
defpred S₁[ object , object ] means ex y being object st
( [$1,y] in FSG & y in Im (FSG,x) & $2 = {$1,y} );
A1: for x being object st x in Im (FSG,x) holds
ex y being object st S₁[x,y]

proof

let y be object ; :: thesis: ( y in Im (FSG,x) implies ex y being object st S₁[y,y] )
assume y in Im (FSG,x) ; :: thesis: ex y being object st S₁[y,y]
then A2: [x,y] in FSG by RELAT_1:169;
then A3: ( x <> y & x in field FSG ) by Lm2, RELAT_1:15;
y in field FSG by A2, RELAT_1:15;
then consider z being object such that
A4: (Im (FSG,x)) /\ (Coim (FSG,y)) = {z} by A3, Def3;
take {y,z} ; :: thesis: S₁[y,{y,z}]
A5: z in {z} by TARSKI:def 1;
Coim (FSG,y) = Im (FSG,y) by Th2;
then z in Im (FSG,y) by A5, A4, XBOOLE_0:def 4;
then A6: [y,z] in FSG by RELAT_1:169;
z in Im (FSG,x) by A5, A4, XBOOLE_0:def 4;
hence S₁[y,{y,z}] by A6; :: thesis: verum

end;

consider h being Function such that
A7: ( dom h = Im (FSG,x) & ( for x being object st x in Im (FSG,x) holds
S₁[x,h . x] ) ) from CLASSES1:sch 1(A1);
reconsider R = rng h as finite set by A7, FINSET_1:8;
set H = h ~ ;
for x being object st x in R holds
card (Im ((h ~),x)) = 2

proof

let y be object ; :: thesis: ( y in R implies card (Im ((h ~),y)) = 2 )
assume y in R ; :: thesis: card (Im ((h ~),y)) = 2
then consider z being object such that
A8: z in dom h and
A9: h . z = y by FUNCT_1:def 3;
consider w being object such that
A10: [z,w] in FSG and
A11: w in Im (FSG,x) and
A12: y = {z,w} by A7, A8, A9;
consider t being object such that
A13: [w,t] in FSG and
A14: t in Im (FSG,x) and
A15: h . w = {w,t} by A11, A7;
t = z

proof

A16: [x,w] in FSG by A11, RELAT_1:169;
then A17: ( x <> w & x in field FSG ) by Lm2, RELAT_1:15;
w in field FSG by A16, RELAT_1:15;
then consider r being object such that
A18: (Im (FSG,x)) /\ (Coim (FSG,w)) = {r} by A17, Def3;
A19: Coim (FSG,w) = Im (FSG,w) by Th2;
then t in Coim (FSG,w) by RELAT_1:169, A13;
then t in {r} by A14, A18, XBOOLE_0:def 4;
then A20: t = r by TARSKI:def 1;
[w,z] in FSG by A10, Lm3;
then z in Coim (FSG,w) by A19, RELAT_1:169;
then z in {r} by A7, A8, A18, XBOOLE_0:def 4;
hence t = z by A20, TARSKI:def 1; :: thesis: verum

end;

then [w,y] in h by A12, A15, A11, A7, FUNCT_1:def 2;
then [y,w] in h ~ by RELAT_1:def 7;
then A21: w in Im ((h ~),y) by RELAT_1:169;
reconsider y = y as set by TARSKI:1;
A22: Im ((h ~),y) c= y

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Im ((h ~),y) or u in y )
assume u in Im ((h ~),y) ; :: thesis: u in y
then [y,u] in h ~ by RELAT_1:169;
then A23: [u,y] in h by RELAT_1:def 7;
then A24: u in dom h by XTUPLE_0:def 12;
then h . u = y by FUNCT_1:def 2, A23;
then ex r being object st
( [u,r] in FSG & r in Im (FSG,x) & y = {u,r} ) by A24, A7;
hence u in y by TARSKI:def 2; :: thesis: verum

end;

[z,y] in h by A8, A9, FUNCT_1:def 2;
then [y,z] in h ~ by RELAT_1:def 7;
then z in Im ((h ~),y) by RELAT_1:169;
then y c= Im ((h ~),y) by A12, A21, ZFMISC_1:32;
then A25: y = Im ((h ~),y) by A22;
z <> w by A10, Lm2;
hence card (Im ((h ~),y)) = 2 by A25, A12, CARD_2:57; :: thesis: verum

end;

then A26: card (h ~) = (card ((h ~) | ((dom (h ~)) \ R))) +` (2 *` (card R)) by SIMPLEX1:1;
dom (h ~) = R by RELAT_1:20;
then (dom (h ~)) \ R = {} by XBOOLE_1:37;
then card ((h ~) | ((dom (h ~)) \ R)) = 0 ;
then card (h ~) = 2 *` (card R) by A26, CARD_2:18;
then 2 * (card R) = card (h ~) by Lm1
.= card h by Th1
.= card (Im (FSG,x)) by A7, CARD_1:62 ;
hence 2 divides card (Im (FSG,x)) by INT_1:def 3; :: thesis: verum