let X be set ; :: thesis: for f being Function st f <> {} & X <> {} holds
product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
let f be Function; :: thesis: ( f <> {} & X <> {} implies product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent )
defpred S₁[ object , object ] means ex g being Function-yielding Function st
( $1 = g & $2 = <:g:> );
assume that
A1: f <> {} and
A2: X <> {} ; :: thesis: product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
A3: for x being object st x in product (Funcs (X,f)) holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in product (Funcs (X,f)) implies ex y being object st S₁[x,y] )
assume x in product (Funcs (X,f)) ; :: thesis: ex y being object st S₁[x,y]
then consider g being Function such that
A4: ( x = g & dom g = dom (Funcs (X,f)) & ( for x being object st x in dom (Funcs (X,f)) holds
g . x in (Funcs (X,f)) . x ) ) by CARD_3:def 5;
g is Function-yielding

proof

let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in dom g or g . x is set )
assume A5: x in dom g ; :: thesis: g . x is set
then A6: g . x in (Funcs (X,f)) . x by A4;
x in dom f by A5, A4, Def8;
then g . x in Funcs (X,(f . x)) by A6, Def8;
hence g . x is Function ; :: thesis: verum

end;

then reconsider g = x as Function-yielding Function by A4;
reconsider y = <:g:> as set ;
take y ; :: thesis: S₁[x,y]
take g ; :: thesis: ( x = g & y = <:g:> )
thus ( x = g & y = <:g:> ) ; :: thesis: verum

end;

consider F being Function such that
A7: ( dom F = product (Funcs (X,f)) & ( for x being object st x in product (Funcs (X,f)) holds
S₁[x,F . x] ) ) from CLASSES1:sch 1(A3);
take F ; :: according to WELLORD2:def 4 :: thesis: ( F is one-to-one & dom F = product (Funcs (X,f)) & rng F = Funcs (X,(product f)) )
A8: for g being Function-yielding Function st g in product (Funcs (X,f)) holds
( dom <:g:> = X & rng g = rng g & rng <:g:> c= product f )

proof

let g be Function-yielding Function; :: thesis: ( g in product (Funcs (X,f)) implies ( dom <:g:> = X & rng g = rng g & rng <:g:> c= product f ) )
A9: dom (Funcs (X,f)) = dom f by Def8;
assume A10: g in product (Funcs (X,f)) ; :: thesis: ( dom <:g:> = X & rng g = rng g & rng <:g:> c= product f )
then A11: dom g = dom (Funcs (X,f)) by CARD_3:9;

A12: now :: thesis: for z being object st z in dom f holds
((dom f) --> X) . z = proj1 (g . z)

let z be object ; :: thesis: ( z in dom f implies ((dom f) --> X) . z = proj1 (g . z) )
assume A13: z in dom f ; :: thesis: ((dom f) --> X) . z = proj1 (g . z)
then ( g . z in (Funcs (X,f)) . z & (Funcs (X,f)) . z = Funcs (X,(f . z)) ) by A10, A9, Def8, CARD_3:9;
then ex h being Function st
( g . z = h & dom h = X & rng h c= f . z ) by FUNCT_2:def 2;
hence ((dom f) --> X) . z = proj1 (g . z) by A13, FUNCOP_1:7; :: thesis: verum

end;

dom ((dom f) --> X) = dom f ;
then doms g = (dom f) --> X by A11, A9, A12, Def1;
then meet (doms g) = X by A1, Th23;
hence A14: ( dom <:g:> = X & rng g = rng g ) by Th25; :: thesis: rng <:g:> c= product f
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng <:g:> or y in product f )
assume y in rng <:g:> ; :: thesis: y in product f
then consider x being object such that
A15: x in dom <:g:> and
A16: y = <:g:> . x by FUNCT_1:def 3;
reconsider h = y as Function by A16;
A17: dom h = dom f by A11, A9, A15, A16, Th26;

now :: thesis: for z being object st z in dom f holds
h . z in f . z

let z be object ; :: thesis: ( z in dom f implies h . z in f . z )
assume A18: z in dom f ; :: thesis: h . z in f . z
then A19: (uncurry g) . (z,x) = h . z by A15, A16, A17, Th26;
( g . z in (Funcs (X,f)) . z & (Funcs (X,f)) . z = Funcs (X,(f . z)) ) by A10, A9, A18, Def8, CARD_3:9;
then consider j being Function such that
A20: g . z = j and
A21: dom j = X and
A22: rng j c= f . z by FUNCT_2:def 2;
A23: j . x in rng j by A14, A15, A21, FUNCT_1:def 3;
(uncurry g) . (z,x) = j . x by A11, A9, A14, A15, A18, A20, A21, FUNCT_5:38;
hence h . z in f . z by A22, A19, A23; :: thesis: verum

end;

hence y in product f by A17, CARD_3:def 5; :: thesis: verum

end;

thus F is one-to-one :: thesis: ( dom F = product (Funcs (X,f)) & rng F = Funcs (X,(product f)) )

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom F or not y in dom F or not F . x = F . y or x = y )
assume that
A24: x in dom F and
A25: y in dom F and
A26: F . x = F . y and
A27: x <> y ; :: thesis: contradiction
consider gy being Function-yielding Function such that
A28: y = gy and
A29: F . y = <:gy:> by A7, A25;
consider gx being Function-yielding Function such that
A30: x = gx and
A31: F . x = <:gx:> by A7, A24;
A32: dom gx = dom (Funcs (X,f)) by A7, A24, A30, CARD_3:9;
A33: dom (Funcs (X,f)) = dom f by Def8;
A34: dom gy = dom (Funcs (X,f)) by A7, A25, A28, CARD_3:9;

now :: thesis: for z being object st z in dom f holds
gx . z = gy . z

let z be object ; :: thesis: ( z in dom f implies gx . z = gy . z )
assume A35: z in dom f ; :: thesis: gx . z = gy . z
then A36: (Funcs (X,f)) . z = Funcs (X,(f . z)) by Def8;
gy . z in (Funcs (X,f)) . z by A7, A25, A28, A33, A35, CARD_3:9;
then consider hy being Function such that
A37: ( gy . z = hy & dom hy = X ) and
rng hy c= f . z by A36, FUNCT_2:def 2;
gx . z in (Funcs (X,f)) . z by A7, A24, A30, A33, A35, CARD_3:9;
then consider hx being Function such that
A38: ( gx . z = hx & dom hx = X ) and
rng hx c= f . z by A36, FUNCT_2:def 2;
A39: dom <:gx:> = X by A7, A8, A24, A30;

now :: thesis: for b being object st b in X holds
hx . b = hy . b

let b be object ; :: thesis: ( b in X implies hx . b = hy . b )
assume A40: b in X ; :: thesis: hx . b = hy . b
reconsider fx = <:gx:> . b as Function ;
A41: ( (uncurry gx) . (z,b) = hx . b & (uncurry gy) . (z,b) = hy . b ) by A32, A34, A33, A35, A38, A37, A40, FUNCT_5:38;
A42: dom fx = dom gx by A39, A40, Th26;
then fx . z = (uncurry gx) . (z,b) by A32, A33, A35, A39, A40, Th26;
hence hx . b = hy . b by A26, A31, A29, A32, A33, A35, A39, A40, A42, A41, Th26; :: thesis: verum

end;

hence gx . z = gy . z by A38, A37; :: thesis: verum

end;

hence contradiction by A27, A30, A28, A32, A34, A33, FUNCT_1:2; :: thesis: verum

end;

thus dom F = product (Funcs (X,f)) by A7; :: thesis: rng F = Funcs (X,(product f))
thus rng F c= Funcs (X,(product f)) :: according to XBOOLE_0:def 10 :: thesis: Funcs (X,(product f)) c= rng F

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in Funcs (X,(product f)) )
assume y in rng F ; :: thesis: y in Funcs (X,(product f))
then consider x being object such that
A43: x in dom F and
A44: y = F . x by FUNCT_1:def 3;
consider g being Function-yielding Function such that
A45: x = g and
A46: y = <:g:> by A7, A43, A44;
( dom <:g:> = X & rng <:g:> c= product f ) by A7, A8, A43, A45;
hence y in Funcs (X,(product f)) by A46, FUNCT_2:def 2; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Funcs (X,(product f)) or y in rng F )
assume y in Funcs (X,(product f)) ; :: thesis: y in rng F
then consider h being Function such that
A47: y = h and
A48: dom h = X and
A49: rng h c= product f by FUNCT_2:def 2;
h is Function-yielding

proof

let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in dom h or h . x is set )
assume x in dom h ; :: thesis: h . x is set
then h . x in rng h by FUNCT_1:3;
then h . x is Element of product f by A49;
hence h . x is set ; :: thesis: verum

end;

then reconsider h = h as Function-yielding Function ;
set g = <:h:>;

A50: now :: thesis: for z being object st z in X holds
(X --> (dom f)) . z = (doms h) . z

let z be object ; :: thesis: ( z in X implies (X --> (dom f)) . z = (doms h) . z )
assume A51: z in X ; :: thesis: (X --> (dom f)) . z = (doms h) . z
then h . z in rng h by A48, FUNCT_1:def 3;
then A52: ex j being Function st
( h . z = j & dom j = dom f & ( for x being object st x in dom f holds
j . x in f . x ) ) by A49, CARD_3:def 5;
thus (X --> (dom f)) . z = dom f by A51, FUNCOP_1:7
.= (doms h) . z by A48, A51, A52, Th18 ; :: thesis: verum

end;

A53: meet (doms h) = dom <:h:> by Th25;
( dom (doms h) = dom h & dom ((dom h) --> (dom f)) = dom h ) by Def1;
then X --> (dom f) = doms h by A48, A50;
then A54: dom <:h:> = dom f by A2, A53, Th23;

A55: now :: thesis: for z being object st z in dom f holds
<:h:> . z in (Funcs (X,f)) . z

let z be object ; :: thesis: ( z in dom f implies <:h:> . z in (Funcs (X,f)) . z )
assume A56: z in dom f ; :: thesis: <:h:> . z in (Funcs (X,f)) . z
reconsider i = <:h:> . z as Function ;
A57: dom i = X by A48, A54, A56, Th26;
rng i c= f . z

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng i or x in f . z )
assume x in rng i ; :: thesis: x in f . z
then consider a being object such that
A58: a in dom i and
A59: x = i . a by FUNCT_1:def 3;
h . a in rng h by A48, A57, A58, FUNCT_1:def 3;
then consider j being Function such that
A60: ( h . a = j & dom j = dom f ) and
A61: for x being object st x in dom f holds
j . x in f . x by A49, CARD_3:def 5;
i . a = (uncurry h) . (a,z) by A54, A56, A58, Th26
.= j . z by A48, A56, A57, A58, A60, FUNCT_5:38 ;
hence x in f . z by A56, A59, A61; :: thesis: verum

end;

then <:h:> . z in Funcs (X,(f . z)) by A57, FUNCT_2:def 2;
hence <:h:> . z in (Funcs (X,f)) . z by A56, Def8; :: thesis: verum

end;

A62: meet (doms <:h:>) = dom <:<:h:>:> by Th25;
product f c= Funcs ((dom f),(Union f)) by Th1;
then A63: rng h c= Funcs ((dom f),(Union f)) by A49;
then A64: dom (uncurry h) = [:(dom h),(dom f):] by FUNCT_5:26;
dom f = dom (Funcs (X,f)) by Def8;
then A65: <:h:> in product (Funcs (X,f)) by A54, A55, CARD_3:def 5;
then A66: ex g9 being Function-yielding Function st
( <:h:> = g9 & F . <:h:> = <:g9:> ) by A7;
dom (uncurry' h) = [:(dom f),(dom h):] by A63, FUNCT_5:26;
then A67: (uncurry' h) | [:(meet (doms h)),(dom h):] = uncurry' h by A53, A54;
A68: ( uncurry' h = ~ (uncurry h) & curry (~ (uncurry h)) = curry' (uncurry h) ) by FUNCT_5:def 3, FUNCT_5:def 4;
dom <:<:h:>:> = X by A8, A65;
then A69: (uncurry h) | [:(meet (doms <:h:>)),(dom <:h:>):] = uncurry h by A48, A54, A64, A62;
uncurry' (curry' (uncurry h)) = uncurry h by A64, FUNCT_5:49;
then <:<:h:>:> = h by A1, A63, A67, A69, A68, FUNCT_5:48;
hence y in rng F by A7, A47, A65, A66, FUNCT_1:def 3; :: thesis: verum