end;

assume A2: dom f <> {} ; :: thesis:
defpred S₂[ set , object ] means ex A being set st
( A = $2 & ( for x being object holds
( x in A iff ( x in Funcs ((card $1),$1) & ex g being Function st
( x = g & rng g = $1 ) ) ) ) );
defpred S₃[ object , object ] means S₂[f . $1,$2];
A3: for x being object st x in dom f holds
ex y being object st S₃[x,y]

let x be object ; :: thesis:
assume x in dom f ; :: thesis:
defpred S₄[ object ] means ex g being Function st
( $1 = g & rng g = f . x );
consider Y being set such that
A4: for z being object holds
( z in Y iff ( z in Funcs ((card (f . x)),(f . x)) & S₄[z] ) ) from XBOOLE_0:sch 1();
take Y ; :: thesis:
S₂[f . x,Y] by A4;
hence S₃[x,Y] ; :: thesis:

end;

consider k being Function such that
A5: ( dom k = dom f & ( for x being object st x in dom f holds
S₃[x,k . x] ) ) from CLASSES1:sch 1(A3);
reconsider M = rng k as non empty set by A2, A5, RELAT_1:42;

let X be set ; :: thesis:
assume X in M ; :: thesis:
then consider x being object such that
A6: x in dom k and
A7: X = k . x by FUNCT_1:def 3;
card (f . x),f . x are_equipotent by CARD_1:def 2;
then consider g being Function such that
g is one-to-one and
A8: dom g = card (f . x) and
A9: rng g = f . x ;
A10: g in Funcs ((card (f . x)),(f . x)) by A8, A9, FUNCT_2:def 2;
S₃[x,k . x] by A5, A6;
hence X <> {} by A7, A9, A10; :: thesis:

end;

then consider FF being Function such that
dom FF = M and
A11: for X being set st X in M holds
FF . X in X by FUNCT_1:111;
set DD = union (rng (disjoin (Card f)));
defpred S₄[ object , object ] means ex g being Function st
( g = FF . (k . ($1 `2)) & $2 = g . ($1 `1) );
A12: for x being object st x in union (rng (disjoin (Card f))) holds
ex y being object st S₄[x,y]

let x be object ; :: thesis:
assume x in union (rng (disjoin (Card f))) ; :: thesis:
then consider X being set such that
A13: x in X and
A14: X in rng (disjoin (Card f)) by TARSKI:def 4;
consider y being object such that
A15: y in dom (disjoin (Card f)) and
A16: X = (disjoin (Card f)) . y by A14, FUNCT_1:def 3;
A17: dom (disjoin (Card f)) = dom (Card f) by Def3;
A18: dom (Card f) = dom f by Def2;
X = [:((Card f) . y),{y}:] by A15, A16, A17, Def3;
then x `2 in {y} by A13, MCART_1:10;
then A19: x `2 in dom f by A15, A17, A18, TARSKI:def 1;
then k . (x `2) in M by A5, FUNCT_1:def 3;
then A20: FF . (k . (x `2)) in k . (x `2) by A11;
S₃[x `2 ,k . (x `2)] by A5, A19;
then FF . (k . (x `2)) in Funcs ((card (f . (x `2))),(f . (x `2))) by A20;
then consider g being Function such that
A21: FF . (k . (x `2)) = g and
dom g = card (f . (x `2)) and
rng g c= f . (x `2) by FUNCT_2:def 2;
take g . (x `1) ; :: thesis:
take g ; :: thesis:
thus ( g = FF . (k . (x `2)) & g . (x `1) = g . (x `1) ) by A21; :: thesis:

end;

consider t being Function such that
A22: ( dom t = union (rng (disjoin (Card f))) & ( for x being object st x in union (rng (disjoin (Card f))) holds
S₄[x,t . x] ) ) from CLASSES1:sch 1(A12);
union (rng f) c= rng t

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union (rng f) ; :: thesis:
then consider X being set such that
A23: x in X and
A24: X in rng f by TARSKI:def 4;
consider y being object such that
A25: y in dom f and
A26: X = f . y by A24, FUNCT_1:def 3;
k . y in M by A5, A25, FUNCT_1:def 3;
then A27: FF . (k . y) in k . y by A11;
A28: S₃[y,k . y] by A5, A25;
then FF . (k . y) in Funcs ((card (f . y)),(f . y)) by A27;
then consider g being Function such that
A29: FF . (k . y) = g and
A30: dom g = card (f . y) and
rng g c= f . y by FUNCT_2:def 2;
ex g being Function st
( FF . (k . y) = g & rng g = f . y ) by A27, A28;
then consider z being object such that
A31: z in dom g and
A32: x = g . z by A23, A26, A29, FUNCT_1:def 3;
A33: (Card f) . y = card (f . y) by A25, Def2;
A34: dom (Card f) = dom f by Def2;
then A35: (disjoin (Card f)) . y = [:(dom g),{y}:] by A25, A30, A33, Def3;
A36: y in {y} by TARSKI:def 1;
A37: dom (disjoin (Card f)) = dom f by A34, Def3;
A38: [z,y] in [:(dom g),{y}:] by A31, A36, ZFMISC_1:87;
[:(dom g),{y}:] in rng (disjoin (Card f)) by A25, A35, A37, FUNCT_1:def 3;
then A39: [z,y] in union (rng (disjoin (Card f))) by A38, TARSKI:def 4;
A40: [z,y] `1 = z ;
[z,y] `2 = y ;
then ex g being Function st
( g = FF . (k . y) & t . [z,y] = g . z ) by A22, A39, A40;
hence x in rng t by A22, A29, A32, A39, FUNCT_1:def 3; :: thesis:

end;

end;