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₁[ set , set ] means ex g being 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 set st x in product (Funcs (X,f)) holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in product (Funcs (X,f)) implies ex y being set st S₁[x,y] )
assume x in product (Funcs (X,f)) ; :: thesis: ex y being set st S₁[x,y]
then ex g being Function st
( x = g & dom g = dom (Funcs (X,f)) & ( for x being set st x in dom (Funcs (X,f)) holds
g . x in (Funcs (X,f)) . x ) ) by CARD_3:def 5;
then reconsider g = x as Function ;
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
A4: ( dom F = product (Funcs (X,f)) & ( for x being set 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 & proj1 F = product (Funcs (X,f)) & proj2 F = Funcs (X,(product f)) )
A5: for g being Function st g in product (Funcs (X,f)) holds
( dom <:g:> = X & SubFuncs (rng g) = rng g & rng <:g:> c= product f )

proof

let g be Function; :: thesis: ( g in product (Funcs (X,f)) implies ( dom <:g:> = X & SubFuncs (rng g) = rng g & rng <:g:> c= product f ) )
A6: g " (rng g) = dom g by RELAT_1:134;
A7: dom (Funcs (X,f)) = dom f by Def9;
assume A8: g in product (Funcs (X,f)) ; :: thesis: ( dom <:g:> = X & SubFuncs (rng g) = rng g & rng <:g:> c= product f )
then A9: dom g = dom (Funcs (X,f)) by CARD_3:9;

A10: now

let a be set ; :: thesis: ( a in rng g implies a is Function )
assume a in rng g ; :: thesis: a is Function
then consider z being set such that
A11: z in dom g and
A12: a = g . z by FUNCT_1:def 3;
( g . z in (Funcs (X,f)) . z & (Funcs (X,f)) . z = Funcs (X,(f . z)) ) by A8, A9, A7, A11, Def9, CARD_3:9;
hence a is Function by A12; :: thesis: verum

end;

then A13: SubFuncs (rng g) = rng g by Lm1;

A14: now

let z be set ; :: thesis: ( z in dom f implies ((dom f) --> X) . z = proj1 (g . z) )
assume A15: 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 A8, A7, Def9, 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 A15, FUNCOP_1:7; :: thesis: verum

end;

dom ((dom f) --> X) = dom f by FUNCOP_1:13;
then doms g = (dom f) --> X by A9, A7, A13, A6, A14, Def2;
then meet (doms g) = X by A1, Th43;
hence A16: ( dom <:g:> = X & SubFuncs (rng g) = rng g ) by A10, Lm1, Th49; :: thesis: rng <:g:> c= product f
let y be set ; :: 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 set such that
A17: x in dom <:g:> and
A18: y = <:g:> . x by FUNCT_1:def 3;
reconsider h = y as Function by A17, A18, Th50;
A19: dom h = dom f by A9, A7, A13, A6, A17, A18, Th51;

now

let z be set ; :: thesis: ( z in dom f implies h . z in f . z )
assume A20: z in dom f ; :: thesis: h . z in f . z
then A21: (uncurry g) . (z,x) = h . z by A17, A18, A19, Th51;
( g . z in (Funcs (X,f)) . z & (Funcs (X,f)) . z = Funcs (X,(f . z)) ) by A8, A7, A20, Def9, CARD_3:9;
then consider j being Function such that
A22: g . z = j and
A23: dom j = X and
A24: rng j c= f . z by FUNCT_2:def 2;
A25: j . x in rng j by A16, A17, A23, FUNCT_1:def 3;
(uncurry g) . (z,x) = j . x by A9, A7, A16, A17, A20, A22, A23, FUNCT_5:38;
hence h . z in f . z by A24, A21, A25; :: thesis: verum

end;

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

end;

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

proof

let x be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not x in proj1 F or not b₁ in proj1 F or not F . x = F . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 F or not y in proj1 F or not F . x = F . y or x = y )
assume that
A26: x in dom F and
A27: y in dom F and
A28: F . x = F . y and
A29: x <> y ; :: thesis: contradiction
consider gy being Function such that
A30: y = gy and
A31: F . y = <:gy:> by A4, A27;
consider gx being Function such that
A32: x = gx and
A33: F . x = <:gx:> by A4, A26;
A34: dom gx = dom (Funcs (X,f)) by A4, A26, A32, CARD_3:9;
A35: dom (Funcs (X,f)) = dom f by Def9;
A36: dom gy = dom (Funcs (X,f)) by A4, A27, A30, CARD_3:9;

now

let z be set ; :: thesis: ( z in dom f implies gx . z = gy . z )
assume A37: z in dom f ; :: thesis: gx . z = gy . z
then A38: (Funcs (X,f)) . z = Funcs (X,(f . z)) by Def9;
gy . z in (Funcs (X,f)) . z by A4, A27, A30, A35, A37, CARD_3:9;
then consider hy being Function such that
A39: ( gy . z = hy & dom hy = X ) and
rng hy c= f . z by A38, FUNCT_2:def 2;
gx . z in (Funcs (X,f)) . z by A4, A26, A32, A35, A37, CARD_3:9;
then consider hx being Function such that
A40: ( gx . z = hx & dom hx = X ) and
rng hx c= f . z by A38, FUNCT_2:def 2;
A41: dom <:gx:> = X by A4, A5, A26, A32;
A42: ( SubFuncs (rng gx) = rng gx & gx " (rng gx) = dom gx ) by A4, A5, A26, A32, RELAT_1:134;

now

let b be set ; :: thesis: ( b in X implies hx . b = hy . b )
assume A43: b in X ; :: thesis: hx . b = hy . b
then reconsider fx = <:gx:> . b as Function by A41, Th50;
A44: ( (uncurry gx) . (z,b) = hx . b & (uncurry gy) . (z,b) = hy . b ) by A34, A36, A35, A37, A40, A39, A43, FUNCT_5:38;
A45: dom fx = dom gx by A41, A42, A43, Th51;
then fx . z = (uncurry gx) . (z,b) by A34, A35, A37, A41, A43, Th51;
hence hx . b = hy . b by A28, A33, A31, A34, A35, A37, A41, A43, A45, A44, Th51; :: thesis: verum

end;

hence gx . z = gy . z by A40, A39, FUNCT_1:2; :: thesis: verum

end;

hence contradiction by A29, A32, A30, A34, A36, A35, FUNCT_1:2; :: thesis: verum

end;

thus dom F = product (Funcs (X,f)) by A4; :: thesis: proj2 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= proj2 F

proof

let y be set ; :: 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 set such that
A46: x in dom F and
A47: y = F . x by FUNCT_1:def 3;
consider g being Function such that
A48: x = g and
A49: y = <:g:> by A4, A46, A47;
( dom <:g:> = X & rng <:g:> c= product f ) by A4, A5, A46, A48;
hence y in Funcs (X,(product f)) by A49, FUNCT_2:def 2; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Funcs (X,(product f)) or y in proj2 F )
assume y in Funcs (X,(product f)) ; :: thesis: y in proj2 F
then consider h being Function such that
A50: y = h and
A51: dom h = X and
A52: rng h c= product f by FUNCT_2:def 2;
set g = <:h:>;
A53: h " (rng h) = dom h by RELAT_1:134;

A54: now

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

end;

A57: meet (doms h) = dom <:h:> by Th49;

now

let z be set ; :: thesis: ( z in rng h implies z is Function )
assume z in rng h ; :: thesis: z is Function
then ex j being Function st
( z = j & dom j = dom f & ( for x being set st x in dom f holds
j . x in f . x ) ) by A52, CARD_3:def 5;
hence z is Function ; :: thesis: verum

end;

then A58: SubFuncs (rng h) = rng h by Lm1;
( dom (doms h) = h " (SubFuncs (rng h)) & dom ((dom h) --> (dom f)) = dom h ) by Def2, FUNCOP_1:13;
then X --> (dom f) = doms h by A51, A58, A53, A54, FUNCT_1:2;
then A59: dom <:h:> = dom f by A2, A57, Th43;

A60: now

let z be set ; :: thesis: ( z in dom f implies <:h:> . z in (Funcs (X,f)) . z )
assume A61: z in dom f ; :: thesis: <:h:> . z in (Funcs (X,f)) . z
then reconsider i = <:h:> . z as Function by A59, Th50;
A62: dom i = X by A51, A58, A53, A59, A61, Th51;
rng i c= f . z

proof

let x be set ; :: 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 set such that
A63: a in dom i and
A64: x = i . a by FUNCT_1:def 3;
h . a in rng h by A51, A62, A63, FUNCT_1:def 3;
then consider j being Function such that
A65: ( h . a = j & dom j = dom f ) and
A66: for x being set st x in dom f holds
j . x in f . x by A52, CARD_3:def 5;
i . a = (uncurry h) . (a,z) by A59, A61, A63, Th51
.= j . z by A51, A61, A62, A63, A65, FUNCT_5:38 ;
hence x in f . z by A61, A64, A66; :: thesis: verum

end;

then <:h:> . z in Funcs (X,(f . z)) by A62, FUNCT_2:def 2;
hence <:h:> . z in (Funcs (X,f)) . z by A61, Def9; :: thesis: verum

end;

A67: meet (doms <:h:>) = dom <:<:h:>:> by Th49;
product f c= Funcs ((dom f),(Union f)) by Th10;
then A68: rng h c= Funcs ((dom f),(Union f)) by A52, XBOOLE_1:1;
then A69: dom (uncurry h) = [:(dom h),(dom f):] by FUNCT_5:26;
dom f = dom (Funcs (X,f)) by Def9;
then A70: <:h:> in product (Funcs (X,f)) by A59, A60, CARD_3:def 5;
then A71: ex g9 being Function st
( <:h:> = g9 & F . <:h:> = <:g9:> ) by A4;
dom (uncurry' h) = [:(dom f),(dom h):] by A68, FUNCT_5:26;
then A72: (uncurry' h) | [:(meet (doms h)),(dom h):] = uncurry' h by A57, A59, RELAT_1:68;
A73: ( uncurry' h = ~ (uncurry h) & curry (~ (uncurry h)) = curry' (uncurry h) ) by FUNCT_5:def 3, FUNCT_5:def 4;
dom <:<:h:>:> = X by A5, A70;
then A74: (uncurry h) | [:(meet (doms <:h:>)),(dom <:h:>):] = uncurry h by A51, A59, A69, A67, RELAT_1:68;
uncurry' (curry' (uncurry h)) = uncurry h by A69, FUNCT_5:49;
then <:<:h:>:> = h by A1, A68, A72, A74, A73, FUNCT_5:48;
hence y in proj2 F by A4, A50, A70, A71, FUNCT_1:def 3; :: thesis: verum