let D, E be non-empty non empty FinSequence; :: thesis: for F being non empty set ex L being Function of (Funcs ((product D),(Funcs ((product E),F)))),(Funcs ((product (E ^ D)),F)) st
( L is bijective & ( for f being Function of (product D),(Funcs ((product E),F))
for e, d being FinSequence st e in product E & d in product D holds
(L . f) . (e ^ d) = (f . d) . e ) )
let F be non empty set ; :: thesis: ex L being Function of (Funcs ((product D),(Funcs ((product E),F)))),(Funcs ((product (E ^ D)),F)) st
( L is bijective & ( for f being Function of (product D),(Funcs ((product E),F))
for e, d being FinSequence st e in product E & d in product D holds
(L . f) . (e ^ d) = (f . d) . e ) )
consider I being Function of (Funcs ((product D),(Funcs ((product E),F)))),(Funcs ([:(product E),(product D):],F)) such that
A1: ( I is bijective & ( for f being Function of (product D),(Funcs ((product E),F))
for e, d being object st e in product E & d in product D holds
(I . f) . (e,d) = (f . d) . e ) ) by Th2;
consider J being Function of [:(product E),(product D):],(product (E ^ D)) such that
A2: ( J is one-to-one & J is onto & ( for x, y being FinSequence st x in product E & y in product D holds
J . (x,y) = x ^ y ) ) by PRVECT_3:6;
A3: rng J = product (E ^ D) by A2, FUNCT_2:def 3;
then reconsider K = J " as Function of (product (E ^ D)),[:(product E),(product D):] by FUNCT_2:25, A2;
deffunc H1( object ) -> set = (I . $1) * K;
A4: for x being object st x in Funcs ((product D),(Funcs ((product E),F))) holds
H1(x) in Funcs ((product (E ^ D)),F)
proof
let x be object ; :: thesis: ( x in Funcs ((product D),(Funcs ((product E),F))) implies H1(x) in Funcs ((product (E ^ D)),F) )
assume x in Funcs ((product D),(Funcs ((product E),F))) ; :: thesis: H1(x) in Funcs ((product (E ^ D)),F)
then A5: I . x in Funcs ([:(product E),(product D):],F) by FUNCT_2:5;
K in Funcs ((product (E ^ D)),[:(product E),(product D):]) by FUNCT_2:8;
hence H1(x) in Funcs ((product (E ^ D)),F) by A5, FUNCT_2:128; :: thesis: verum
end;
consider L being Function of (Funcs ((product D),(Funcs ((product E),F)))),(Funcs ((product (E ^ D)),F)) such that
A6: for e being object st e in Funcs ((product D),(Funcs ((product E),F))) holds
L . e = H1(e) from FUNCT_2:sch 2(A4);
 A7: K * J = id [:(product E),(product D):] by A2, A3, FUNCT_2:29;
A8: J * K = id (product (E ^ D)) by A2, A3, FUNCT_2:29;
now :: thesis: for z1, z2 being object st z1 in Funcs ((product D),(Funcs ((product E),F))) & z2 in Funcs ((product D),(Funcs ((product E),F))) & L . z1 = L . z2 holds
z1 = z2
let z1, z2 be object ; :: thesis: ( z1 in Funcs ((product D),(Funcs ((product E),F))) & z2 in Funcs ((product D),(Funcs ((product E),F))) & L . z1 = L . z2 implies z1 = z2 )
assume A9: ( z1 in Funcs ((product D),(Funcs ((product E),F))) & z2 in Funcs ((product D),(Funcs ((product E),F))) & L . z1 = L . z2 ) ; :: thesis: z1 = z2
(I . z1) * K = L . z2 by A6, A9;
then A10: ((I . z1) * K) * J = ((I . z2) * K) * J by A6, A9;
(I . z1) * (K * J) = ((I . z1) * K) * J by RELAT_1:36;
then A11: (I . z1) * (K * J) = (I . z2) * (K * J) by A10, RELAT_1:36;
( I . z1 is Function of [:(product E),(product D):],F & I . z2 is Function of [:(product E),(product D):],F ) by A9, FUNCT_2:5, FUNCT_2:66;
then ( (I . z1) * (K * J) = I . z1 & (I . z2) * (K * J) = I . z2 ) by A7, FUNCT_2:17;
hence z1 = z2 by A1, FUNCT_2:19, A9, A11; :: thesis: verum
end;
then A12: L is one-to-one by FUNCT_2:19;
now :: thesis: for w being object st w in Funcs ((product (E ^ D)),F) holds
w in rng L
let w be object ; :: thesis: ( w in Funcs ((product (E ^ D)),F) implies w in rng L )
assume w in Funcs ((product (E ^ D)),F) ; :: thesis: w in rng L
then reconsider wf = w as Function of (product (E ^ D)),F by FUNCT_2:66;
wf * J in Funcs ([:(product E),(product D):],F) by FUNCT_2:8;
then wf * J in rng I by A1, FUNCT_2:def 3;
then consider zf being object such that
A13: ( zf in Funcs ((product D),(Funcs ((product E),F))) & I . zf = wf * J ) by FUNCT_2:11;
L . zf = (wf * J) * K by A6, A13;
then L . zf = wf * (id (product (E ^ D))) by A8, RELAT_1:36;
then L . zf = w by FUNCT_2:17;
hence w in rng L by A13, FUNCT_2:112; :: thesis: verum
end;
then Funcs ((product (E ^ D)),F) c= rng L by TARSKI:def 3;
then A14: L is onto by FUNCT_2:def 3, XBOOLE_0:def 10;
for f being Function of (product D),(Funcs ((product E),F))
for e, d being FinSequence st e in product E & d in product D holds
(L . f) . (e ^ d) = (f . d) . e
proof
let f be Function of (product D),(Funcs ((product E),F)); :: thesis: for e, d being FinSequence st e in product E & d in product D holds
(L . f) . (e ^ d) = (f . d) . e
let e, d be FinSequence; :: thesis: ( e in product E & d in product D implies (L . f) . (e ^ d) = (f . d) . e )
assume A15: ( e in product E & d in product D ) ; :: thesis: (L . f) . (e ^ d) = (f . d) . e
then A16: (I . f) . (e,d) = (f . d) . e by A1;
A17: J . (e,d) = e ^ d by A2, A15;
A18: [e,d] in [:(product E),(product D):] by A15, ZFMISC_1:87;
A19: K . (J . (e,d)) = [e,d] by FUNCT_2:26, A2, A15, ZFMISC_1:87;
f in Funcs ((product D),(Funcs ((product E),F))) by FUNCT_2:8;
then (L . f) . (e ^ d) = ((I . f) * K) . (J . (e,d)) by A17, A6;
hence (L . f) . (e ^ d) = (f . d) . e by A16, A19, A18, FUNCT_2:5, FUNCT_2:15; :: thesis: verum
end;
hence ex L being Function of (Funcs ((product D),(Funcs ((product E),F)))),(Funcs ((product (E ^ D)),F)) st
( L is bijective & ( for f being Function of (product D),(Funcs ((product E),F))
for e, d being FinSequence st e in product E & d in product D holds
(L . f) . (e ^ d) = (f . d) . e ) ) by A12, A14; :: thesis: verum