let F, G be Function; :: thesis: ( F,G are_fiberwise_equipotent iff ex H being Function st
( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H ) )
thus ( F,G are_fiberwise_equipotent implies ex H being Function st
( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H ) ) :: thesis: ( ex H being Function st
( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H ) implies F,G are_fiberwise_equipotent )
proof
assume A1: F,G are_fiberwise_equipotent ; :: thesis: ex H being Function st
( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H )
defpred S1[ set , set ] means ( $2 is Function & ( for f being Function st $2 = f holds
( dom f = F " {$1} & rng f = G " {$1} & f is one-to-one ) ) );
A2: for x being set st x in rng F holds
ex y being set st S1[x,y]
proof
let x be set ; :: thesis: ( x in rng F implies ex y being set st S1[x,y] )
assume x in rng F ; :: thesis: ex y being set st S1[x,y]
card (Coim F,x) = card (Coim G,x) by A1, Def1;
then F " {x},G " {x} are_equipotent by CARD_1:21;
then consider H being Function such that
A3: ( H is one-to-one & dom H = F " {x} & rng H = G " {x} ) by WELLORD2:def 4;
take H ; :: thesis: S1[x,H]
thus H is Function ; :: thesis: for f being Function st H = f holds
( dom f = F " {x} & rng f = G " {x} & f is one-to-one )
let g be Function; :: thesis: ( H = g implies ( dom g = F " {x} & rng g = G " {x} & g is one-to-one ) )
assume g = H ; :: thesis: ( dom g = F " {x} & rng g = G " {x} & g is one-to-one )
hence ( dom g = F " {x} & rng g = G " {x} & g is one-to-one ) by A3; :: thesis: verum
end;
consider W being Function such that
A4: ( dom W = rng F & ( for x being set st x in rng F holds
S1[x,W . x] ) ) from CLASSES1:sch 1(A2);
 defpred S2[ set , set ] means for H being Function st H = W . (F . $1) holds
$2 = H . $1;
set df = dom F;
set dg = dom G;
A5: for x being set st x in dom F holds
ex y being set st
( y in dom G & S2[x,y] )
proof
let x be set ; :: thesis: ( x in dom F implies ex y being set st
( y in dom G & S2[x,y] ) )
assume A6: x in dom F ; :: thesis: ex y being set st
( y in dom G & S2[x,y] )
then A7: F . x in rng F by FUNCT_1:def 5;
then reconsider f = W . (F . x) as Function by A4;
A8: ( dom f = F " {(F . x)} & rng f = G " {(F . x)} & f is one-to-one ) by A4, A7;
take y = f . x; :: thesis: ( y in dom G & S2[x,y] )
F . x in {(F . x)} by TARSKI:def 1;
then x in F " {(F . x)} by A6, FUNCT_1:def 13;
then f . x in G " {(F . x)} by A8, FUNCT_1:def 5;
hence y in dom G by FUNCT_1:def 13; :: thesis: S2[x,y]
let g be Function; :: thesis: ( g = W . (F . x) implies y = g . x )
assume g = W . (F . x) ; :: thesis: y = g . x
hence y = g . x ; :: thesis: verum
end;
consider IT being Function such that
A9: ( dom IT = dom F & rng IT c= dom G & ( for x being set st x in dom F holds
S2[x,IT . x] ) ) from WELLORD2:sch 1(A5);
 take IT ; :: thesis: ( dom IT = dom F & rng IT = dom G & IT is one-to-one & F = G * IT )
thus dom IT = dom F by A9; :: thesis: ( rng IT = dom G & IT is one-to-one & F = G * IT )
dom G c= rng IT
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom G or x in rng IT )
assume A10: x in dom G ; :: thesis: x in rng IT
then A11: ( G . x in rng G & rng F = rng G ) by A1, Th1, FUNCT_1:def 5;
then reconsider f = W . (G . x) as Function by A4;
A12: ( f is one-to-one & dom f = F " {(G . x)} & rng f = G " {(G . x)} ) by A4, A11;
G . x in {(G . x)} by TARSKI:def 1;
then x in rng f by A10, A12, FUNCT_1:def 13;
then consider z being set such that
A13: ( z in dom f & f . z = x ) by FUNCT_1:def 5;
A14: ( z in dom F & F . z in {(G . x)} ) by A12, A13, FUNCT_1:def 13;
then F . z = G . x by TARSKI:def 1;
then IT . z = x by A9, A13, A14;
hence x in rng IT by A9, A14, FUNCT_1:def 5; :: thesis: verum
end;
hence rng IT = dom G by A9, XBOOLE_0:def 10; :: thesis: ( IT is one-to-one & F = G * IT )
now
let x, y be set ; :: thesis: ( x in dom IT & y in dom IT & IT . x = IT . y implies x = y )
assume A15: ( x in dom IT & y in dom IT & IT . x = IT . y ) ; :: thesis: x = y
then A16: ( F . x in rng F & F . y in rng F ) by A9, FUNCT_1:def 5;
then reconsider f1 = W . (F . x), f2 = W . (F . y) as Function by A4;
A17: ( IT . x = f1 . x & IT . y = f2 . y ) by A9, A15;
A18: ( dom f1 = F " {(F . x)} & rng f1 = G " {(F . x)} & f1 is one-to-one & dom f2 = F " {(F . y)} & rng f2 = G " {(F . y)} & f2 is one-to-one ) by A4, A16;
( F . x in {(F . x)} & F . y in {(F . y)} ) by TARSKI:def 1;
then A19: ( x in F " {(F . x)} & y in F " {(F . y)} ) by A9, A15, FUNCT_1:def 13;
then ( f1 . x in rng f1 & f2 . y in rng f2 ) by A18, FUNCT_1:def 5;
then f1 . x in (G " {(F . x)}) /\ (G " {(F . y)}) by A15, A17, A18, XBOOLE_0:def 4;
then f1 . x in G " ({(F . x)} /\ {(F . y)}) by FUNCT_1:137;
then G . (f1 . x) in {(F . x)} /\ {(F . y)} by FUNCT_1:def 13;
then ( G . (f1 . x) in {(F . x)} & G . (f1 . x) in {(F . y)} ) by XBOOLE_0:def 4;
then ( G . (f1 . x) = F . x & G . (f1 . x) = F . y ) by TARSKI:def 1;
hence x = y by A15, A17, A18, A19, FUNCT_1:def 8; :: thesis: verum
end;
hence IT is one-to-one by FUNCT_1:def 8; :: thesis: F = G * IT
A20: dom (G * IT) = dom F by A9, RELAT_1:46;
now
let x be set ; :: thesis: ( x in dom F implies F . x = (G * IT) . x )
assume A21: x in dom F ; :: thesis: F . x = (G * IT) . x
then A22: F . x in rng F by FUNCT_1:def 5;
then reconsider f = W . (F . x) as Function by A4;
A23: ( f is one-to-one & dom f = F " {(F . x)} & rng f = G " {(F . x)} ) by A4, A22;
F . x in {(F . x)} by TARSKI:def 1;
then x in F " {(F . x)} by A21, FUNCT_1:def 13;
then f . x in G " {(F . x)} by A23, FUNCT_1:def 5;
then G . (f . x) in {(F . x)} by FUNCT_1:def 13;
then A24: G . (f . x) = F . x by TARSKI:def 1;
IT . x = f . x by A9, A21;
hence F . x = (G * IT) . x by A9, A21, A24, FUNCT_1:23; :: thesis: verum
end;
hence F = G * IT by A20, FUNCT_1:9; :: thesis: verum
end;
given H being Function such that A25: ( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H ) ; :: thesis: F,G are_fiberwise_equipotent
let x be set ; :: according to CLASSES1:def 9 :: thesis: card (Coim F,x) = card (Coim G,x)
set t = H | (F " {x});
A26: H | (F " {x}) is one-to-one by A25, FUNCT_1:84;
A27: dom (H | (F " {x})) = F " {x} by A25, RELAT_1:91, RELAT_1:167;
rng (H | (F " {x})) = G " {x}
proof
thus rng (H | (F " {x})) c= G " {x} :: according to XBOOLE_0:def 10 :: thesis: G " {x} c= rng (H | (F " {x}))
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (H | (F " {x})) or z in G " {x} )
assume z in rng (H | (F " {x})) ; :: thesis: z in G " {x}
then consider y being set such that
A28: ( y in dom (H | (F " {x})) & (H | (F " {x})) . y = z ) by FUNCT_1:def 5;
F . y in {x} by A27, A28, FUNCT_1:def 13;
then A29: F . y = x by TARSKI:def 1;
A30: z = H . y by A28, FUNCT_1:70;
dom (H | (F " {x})) = (dom H) /\ (F " {x}) by RELAT_1:90;
then A31: y in dom H by A28, XBOOLE_0:def 4;
then A32: z in dom G by A25, A30, FUNCT_1:def 5;
x = G . z by A25, A29, A30, A31, FUNCT_1:23;
then G . z in {x} by TARSKI:def 1;
hence z in G " {x} by A32, FUNCT_1:def 13; :: thesis: verum
end;
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in G " {x} or z in rng (H | (F " {x})) )
assume z in G " {x} ; :: thesis: z in rng (H | (F " {x}))
then A33: ( z in dom G & G . z in {x} ) by FUNCT_1:def 13;
then A34: G . z = x by TARSKI:def 1;
consider y being set such that
A35: ( y in dom H & H . y = z ) by A25, A33, FUNCT_1:def 5;
F . y = x by A25, A34, A35, FUNCT_1:23;
then F . y in {x} by TARSKI:def 1;
then A36: y in dom (H | (F " {x})) by A25, A27, A35, FUNCT_1:def 13;
then (H | (F " {x})) . y in rng (H | (F " {x})) by FUNCT_1:def 5;
hence z in rng (H | (F " {x})) by A35, A36, FUNCT_1:70; :: thesis: verum
end;
then F " {x},G " {x} are_equipotent by A26, A27, WELLORD2:def 4;
hence card (Coim F,x) = card (Coim G,x) by CARD_1:21; :: thesis: verum