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[ object , object ] 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 object st x in rng F holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in rng F implies ex y being object st S1[x,y] )
assume x in rng F ; :: thesis: ex y being object st S1[x,y]
card (Coim (F,x)) = card (Coim (G,x)) by A1;
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, CARD_1:5;
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 object st x in rng F holds
S1[x,W . x] ) ) from CLASSES1:sch 1(A2);
 defpred S2[ object , object ] 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 object st x in dom F holds
ex y being object st
( y in dom G & S2[x,y] )
proof
let x be object ; :: thesis: ( x in dom F implies ex y being object st
( y in dom G & S2[x,y] ) )
assume A6: x in dom F ; :: thesis: ex y being object st
( y in dom G & S2[x,y] )
then A7: F . x in rng F by FUNCT_1:def 3;
then reconsider f = W . (F . x) as Function by A4;
A8: ( dom f = F " {(F . x)} & rng f = G " {(F . x)} ) 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 7;
then f . x in G " {(F . x)} by A8, FUNCT_1:def 3;
hence y in dom G by FUNCT_1:def 7; :: 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 object st x in dom F holds
S2[x,IT . x] ) ) from FUNCT_1:sch 6(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 object ; :: 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 by FUNCT_1:def 3;
A12: rng F = rng G by A1, Th75;
then reconsider f = W . (G . x) as Function by A4, A11;
A13: dom f = F " {(G . x)} by A4, A11, A12;
A14: rng f = G " {(G . x)} by A4, A11, A12;
G . x in {(G . x)} by TARSKI:def 1;
then x in rng f by A10, A14, FUNCT_1:def 7;
then consider z being object such that
A15: z in dom f and
A16: f . z = x by FUNCT_1:def 3;
A17: z in dom F by A13, A15, FUNCT_1:def 7;
F . z in {(G . x)} by A13, A15, FUNCT_1:def 7;
then F . z = G . x by TARSKI:def 1;
then IT . z = x by A9, A16, A17;
hence x in rng IT by A9, A17, FUNCT_1:def 3; :: thesis: verum
end;
hence rng IT = dom G by A9; :: thesis: ( IT is one-to-one & F = G * IT )
now :: thesis: for x, y being object st x in dom IT & y in dom IT & IT . x = IT . y holds
x = y
let x, y be object ; :: thesis: ( x in dom IT & y in dom IT & IT . x = IT . y implies x = y )
assume that
A18: x in dom IT and
A19: y in dom IT and
A20: IT . x = IT . y ; :: thesis: x = y
A21: F . x in rng F by A9, A18, FUNCT_1:def 3;
A22: F . y in rng F by A9, A19, FUNCT_1:def 3;
then reconsider f1 = W . (F . x), f2 = W . (F . y) as Function by A4, A21;
A23: ( IT . x = f1 . x & IT . y = f2 . y ) by A9, A18, A19;
A24: dom f1 = F " {(F . x)} by A4, A21;
A25: rng f1 = G " {(F . x)} by A4, A21;
A26: f1 is one-to-one by A4, A21;
A27: dom f2 = F " {(F . y)} by A4, A22;
A28: rng f2 = G " {(F . y)} by A4, A22;
A29: F . x in {(F . x)} by TARSKI:def 1;
A30: F . y in {(F . y)} by TARSKI:def 1;
A31: x in F " {(F . x)} by A9, A18, A29, FUNCT_1:def 7;
A32: y in F " {(F . y)} by A9, A19, A30, FUNCT_1:def 7;
A33: f1 . x in rng f1 by A24, A31, FUNCT_1:def 3;
f2 . y in rng f2 by A27, A32, FUNCT_1:def 3;
then f1 . x in (G " {(F . x)}) /\ (G " {(F . y)}) by A20, A23, A25, A28, A33, XBOOLE_0:def 4;
then f1 . x in G " ({(F . x)} /\ {(F . y)}) by FUNCT_1:68;
then A34: G . (f1 . x) in {(F . x)} /\ {(F . y)} by FUNCT_1:def 7;
then A35: G . (f1 . x) in {(F . x)} by XBOOLE_0:def 4;
A36: G . (f1 . x) in {(F . y)} by A34, XBOOLE_0:def 4;
A37: G . (f1 . x) = F . x by A35, TARSKI:def 1;
G . (f1 . x) = F . y by A36, TARSKI:def 1;
hence x = y by A20, A23, A24, A26, A31, A32, A37; :: thesis: verum
end;
hence IT is one-to-one ; :: thesis: F = G * IT
A38: dom (G * IT) = dom F by A9, RELAT_1:27;
now :: thesis: for x being object st x in dom F holds
F . x = (G * IT) . x
let x be object ; :: thesis: ( x in dom F implies F . x = (G * IT) . x )
assume A39: x in dom F ; :: thesis: F . x = (G * IT) . x
then A40: F . x in rng F by FUNCT_1:def 3;
then reconsider f = W . (F . x) as Function by A4;
A41: ( dom f = F " {(F . x)} & rng f = G " {(F . x)} ) by A4, A40;
F . x in {(F . x)} by TARSKI:def 1;
then x in F " {(F . x)} by A39, FUNCT_1:def 7;
then f . x in G " {(F . x)} by A41, FUNCT_1:def 3;
then G . (f . x) in {(F . x)} by FUNCT_1:def 7;
then A42: G . (f . x) = F . x by TARSKI:def 1;
IT . x = f . x by A9, A39;
hence F . x = (G * IT) . x by A9, A39, A42, FUNCT_1:13; :: thesis: verum
end;
hence F = G * IT by A38; :: thesis: verum
end;
given H being Function such that A43: dom H = dom F and
A44: rng H = dom G and
A45: H is one-to-one and
A46: F = G * H ; :: thesis: F,G are_fiberwise_equipotent
let x be object ; :: according to CLASSES1:def 10 :: thesis: card (Coim (F,x)) = card (Coim (G,x))
set t = H | (F " {x});
A47: H | (F " {x}) is one-to-one by A45, FUNCT_1:52;
A48: dom (H | (F " {x})) = F " {x} by A43, RELAT_1:62, RELAT_1:132;
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 object ; :: 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 object such that
A49: y in dom (H | (F " {x})) and
A50: (H | (F " {x})) . y = z by FUNCT_1:def 3;
F . y in {x} by A48, A49, FUNCT_1:def 7;
then A51: F . y = x by TARSKI:def 1;
A52: z = H . y by A49, A50, FUNCT_1:47;
dom (H | (F " {x})) = (dom H) /\ (F " {x}) by RELAT_1:61;
then A53: y in dom H by A49, XBOOLE_0:def 4;
then A54: z in dom G by A44, A52, FUNCT_1:def 3;
x = G . z by A46, A51, A52, A53, FUNCT_1:13;
then G . z in {x} by TARSKI:def 1;
hence z in G " {x} by A54, FUNCT_1:def 7; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in G " {x} or z in rng (H | (F " {x})) )
assume A55: z in G " {x} ; :: thesis: z in rng (H | (F " {x}))
then A56: z in dom G by FUNCT_1:def 7;
G . z in {x} by A55, FUNCT_1:def 7;
then A57: G . z = x by TARSKI:def 1;
consider y being object such that
A58: y in dom H and
A59: H . y = z by A44, A56, FUNCT_1:def 3;
F . y = x by A46, A57, A58, A59, FUNCT_1:13;
then F . y in {x} by TARSKI:def 1;
then A60: y in dom (H | (F " {x})) by A43, A48, A58, FUNCT_1:def 7;
then (H | (F " {x})) . y in rng (H | (F " {x})) by FUNCT_1:def 3;
hence z in rng (H | (F " {x})) by A59, A60, FUNCT_1:47; :: thesis: verum
end;
hence card (Coim (F,x)) = card (Coim (G,x)) by CARD_1:5, A47, A48, WELLORD2:def 4; :: thesis: verum