let D, E, F be non empty set ; :: thesis: ex I being Function of (Funcs (D,(Funcs (E,F)))),(Funcs ([:E,D:],F)) st
( I is bijective & ( for f being Function of D,(Funcs (E,F))
for e, d being object st e in E & d in D holds
(I . f) . (e,d) = (f . d) . e ) )
defpred S₁[ object , object ] means ex f being Function of D,(Funcs (E,F)) ex g being Function of [:E,D:],F st
( $1 = f & $2 = g & ( for e, d being object st e in E & d in D holds
g . (e,d) = (f . d) . e ) );
A1: for x being object st x in Funcs (D,(Funcs (E,F))) holds
ex y being object st
( y in Funcs ([:E,D:],F) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in Funcs (D,(Funcs (E,F))) implies ex y being object st
( y in Funcs ([:E,D:],F) & S₁[x,y] ) )
assume x in Funcs (D,(Funcs (E,F))) ; :: thesis: ex y being object st
( y in Funcs ([:E,D:],F) & S₁[x,y] )
then consider f being Function such that
A2: ( x = f & dom f = D & rng f c= Funcs (E,F) ) by FUNCT_2:def 2;
reconsider f = f as Function of D,(Funcs (E,F)) by FUNCT_2:2, A2;
deffunc H₁( object , object ) -> set = (f . $2) . $1;
A3: for y, x being object st y in E & x in D holds
H₁(y,x) in F

proof

let e, d be object ; :: thesis: ( e in E & d in D implies H₁(e,d) in F )
assume A4: ( e in E & d in D ) ; :: thesis: H₁(e,d) in F
then f . d is Function of E,F by FUNCT_2:5, FUNCT_2:66;
hence H₁(e,d) in F by A4, FUNCT_2:5; :: thesis: verum

end;

consider g being Function of [:E,D:],F such that
A5: for y, x being object st y in E & x in D holds
g . (y,x) = H₁(y,x) from BINOP_1:sch 2(A3);
g in Funcs ([:E,D:],F) by FUNCT_2:8;
hence ex y being object st
( y in Funcs ([:E,D:],F) & S₁[x,y] ) by A2, A5; :: thesis: verum

end;

consider I being Function of (Funcs (D,(Funcs (E,F)))),(Funcs ([:E,D:],F)) such that
A6: for x being object st x in Funcs (D,(Funcs (E,F))) holds
S₁[x,I . x] from FUNCT_2:sch 1(A1);
A7: for f being Function of D,(Funcs (E,F))
for e, d being object st e in E & d in D holds
(I . f) . (e,d) = (f . d) . e

proof

let f be Function of D,(Funcs (E,F)); :: thesis: for e, d being object st e in E & d in D holds
(I . f) . (e,d) = (f . d) . e
let e, d be object ; :: thesis: ( e in E & d in D implies (I . f) . (e,d) = (f . d) . e )
assume A8: ( e in E & d in D ) ; :: thesis: (I . f) . (e,d) = (f . d) . e
f in Funcs (D,(Funcs (E,F))) by FUNCT_2:8;
then ex f0 being Function of D,(Funcs (E,F)) ex g0 being Function of [:E,D:],F st
( f = f0 & I . f = g0 & ( for e, d being object st e in E & d in D holds
g0 . (e,d) = (f0 . d) . e ) ) by A6;
hence (I . f) . (e,d) = (f . d) . e by A8; :: thesis: verum

end;

now :: thesis: for z1, z2 being object st z1 in Funcs (D,(Funcs (E,F))) & z2 in Funcs (D,(Funcs (E,F))) & I . z1 = I . z2 holds
z1 = z2

let z1, z2 be object ; :: thesis: ( z1 in Funcs (D,(Funcs (E,F))) & z2 in Funcs (D,(Funcs (E,F))) & I . z1 = I . z2 implies z1 = z2 )
assume A9: ( z1 in Funcs (D,(Funcs (E,F))) & z2 in Funcs (D,(Funcs (E,F))) & I . z1 = I . z2 ) ; :: thesis: z1 = z2
then reconsider z1f = z1, z2f = z2 as Function of D,(Funcs (E,F)) by FUNCT_2:66;

now :: thesis: for d being object st d in D holds
z1f . d = z2f . d

let d be object ; :: thesis: ( d in D implies z1f . d = z2f . d )
assume A10: d in D ; :: thesis: z1f . d = z2f . d
then A11: ( z1f . d is Function of E,F & z2f . d is Function of E,F ) by FUNCT_2:5, FUNCT_2:66;

now :: thesis: for e being object st e in E holds
(z1f . d) . e = (z2f . d) . e

let e be object ; :: thesis: ( e in E implies (z1f . d) . e = (z2f . d) . e )
assume A12: e in E ; :: thesis: (z1f . d) . e = (z2f . d) . e
then (z1f . d) . e = (I . z2f) . (e,d) by A7, A10, A9;
hence (z1f . d) . e = (z2f . d) . e by A7, A10, A12; :: thesis: verum

end;

hence z1f . d = z2f . d by A11, FUNCT_2:12; :: thesis: verum

end;

hence z1 = z2 by FUNCT_2:12; :: thesis: verum

end;

then A13: I is one-to-one by FUNCT_2:19;

now :: thesis: for w being object st w in Funcs ([:E,D:],F) holds
w in rng I

let w be object ; :: thesis: ( w in Funcs ([:E,D:],F) implies w in rng I )
assume w in Funcs ([:E,D:],F) ; :: thesis: w in rng I
then reconsider wf = w as Function of [:E,D:],F by FUNCT_2:66;
defpred S₂[ object , object ] means ex f being Function of E,F st
( $2 = f & ( for e being object st e in E holds
f . e = wf . (e,$1) ) );
A14: for d being object st d in D holds
ex y being object st
( y in Funcs (E,F) & S₂[d,y] )

proof

let d be object ; :: thesis: ( d in D implies ex y being object st
( y in Funcs (E,F) & S₂[d,y] ) )
assume A15: d in D ; :: thesis: ex y being object st
( y in Funcs (E,F) & S₂[d,y] )
deffunc H₁( object ) -> set = wf . ($1,d);
A16: for e being object st e in E holds
H₁(e) in F

proof

let e be object ; :: thesis: ( e in E implies H₁(e) in F )
assume e in E ; :: thesis: H₁(e) in F
then [e,d] in [:E,D:] by A15, ZFMISC_1:def 2;
hence H₁(e) in F by FUNCT_2:5; :: thesis: verum

end;

consider f being Function of E,F such that
A17: for e being object st e in E holds
f . e = H₁(e) from FUNCT_2:sch 2(A16);
f in Funcs (E,F) by FUNCT_2:8;
hence ex y being object st
( y in Funcs (E,F) & S₂[d,y] ) by A17; :: thesis: verum

end;

consider zf being Function of D,(Funcs (E,F)) such that
A18: for d being object st d in D holds
S₂[d,zf . d] from FUNCT_2:sch 1(A14);
A19: zf in Funcs (D,(Funcs (E,F))) by FUNCT_2:8;

A20: now :: thesis: for e, d being set st e in E & d in D holds
(I . zf) . (e,d) = wf . (e,d)

let e, d be set ; :: thesis: ( e in E & d in D implies (I . zf) . (e,d) = wf . (e,d) )
assume A21: ( e in E & d in D ) ; :: thesis: (I . zf) . (e,d) = wf . (e,d)
then A22: (I . zf) . (e,d) = (zf . d) . e by A7;
ex L being Function of E,F st
( zf . d = L & ( for e being object st e in E holds
L . e = wf . (e,d) ) ) by A18, A21;
hence (I . zf) . (e,d) = wf . (e,d) by A22, A21; :: thesis: verum

end;

I . zf is Function of [:E,D:],F by A19, FUNCT_2:5, FUNCT_2:66;
then I . zf = w by BINOP_1:1, A20;
hence w in rng I by A19, FUNCT_2:112; :: thesis: verum

end;

then Funcs ([:E,D:],F) c= rng I by TARSKI:def 3;
then I is onto by FUNCT_2:def 3, XBOOLE_0:def 10;
hence ex I being Function of (Funcs (D,(Funcs (E,F)))),(Funcs ([:E,D:],F)) st
( I is bijective & ( for f being Function of D,(Funcs (E,F))
for e, d being object st e in E & d in D holds
(I . f) . (e,d) = (f . d) . e ) ) by A7, A13; :: thesis: verum