let D be non empty set ; :: thesis: for E being non-empty non empty FinSequence
for F being non empty set ex L being Function of (Funcs (D,(Funcs ((product E),F)))),(Funcs ((product (E ^ <*D*>)),F)) st
( L is bijective & ( for f being Function of D,(Funcs ((product E),F))
for e being FinSequence
for d being object st e in product E & d in D holds
(L . f) . (e ^ <*d*>) = (f . d) . e ) )
let E be non-empty non empty FinSequence; :: thesis: for F being non empty set ex L being Function of (Funcs (D,(Funcs ((product E),F)))),(Funcs ((product (E ^ <*D*>)),F)) st
( L is bijective & ( for f being Function of D,(Funcs ((product E),F))
for e being FinSequence
for d being object st e in product E & d in D holds
(L . f) . (e ^ <*d*>) = (f . d) . e ) )
let F be non empty set ; :: thesis: ex L being Function of (Funcs (D,(Funcs ((product E),F)))),(Funcs ((product (E ^ <*D*>)),F)) st
( L is bijective & ( for f being Function of D,(Funcs ((product E),F))
for e being FinSequence
for d being object st e in product E & d in D holds
(L . f) . (e ^ <*d*>) = (f . d) . e ) )
consider I being Function of (Funcs (D,(Funcs ((product E),F)))),(Funcs ([:(product E),D:],F)) such that
A1: ( I is bijective & ( for f being Function of D,(Funcs ((product E),F))
for e, d being object st e in product E & d in D holds
(I . f) . (e,d) = (f . d) . e ) ) by Th2;
consider J being Function of [:(product E),D:],(product (E ^ <*D*>)) such that
A2: ( J is bijective & ( for x being FinSequence
for y being object st x in product E & y in D holds
J . (x,y) = x ^ <*y*> ) ) by Th5;
A3: rng J = product (E ^ <*D*>) by A2, FUNCT_2:def 3;
then reconsider K = J " as Function of (product (E ^ <*D*>)),[:(product E),D:] by FUNCT_2:25, A2;
deffunc H₁( object ) -> set = (I . $1) * K;
A4: for x being object st x in Funcs (D,(Funcs ((product E),F))) holds
H₁(x) in Funcs ((product (E ^ <*D*>)),F)

proof

let x be object ; :: thesis: ( x in Funcs (D,(Funcs ((product E),F))) implies H₁(x) in Funcs ((product (E ^ <*D*>)),F) )
assume x in Funcs (D,(Funcs ((product E),F))) ; :: thesis: H₁(x) in Funcs ((product (E ^ <*D*>)),F)
then ( I . x in Funcs ([:(product E),D:],F) & K in Funcs ((product (E ^ <*D*>)),[:(product E),D:]) ) by FUNCT_2:5, FUNCT_2:8;
hence H₁(x) in Funcs ((product (E ^ <*D*>)),F) by FUNCT_2:128; :: thesis: verum

end;

consider L being Function of (Funcs (D,(Funcs ((product E),F)))),(Funcs ((product (E ^ <*D*>)),F)) such that
A5: for e being object st e in Funcs (D,(Funcs ((product E),F))) holds
L . e = H₁(e) from FUNCT_2:sch 2(A4);
take L ; :: thesis: ( L is bijective & ( for f being Function of D,(Funcs ((product E),F))
for e being FinSequence
for d being object st e in product E & d in D holds
(L . f) . (e ^ <*d*>) = (f . d) . e ) )
A6: K * J = id [:(product E),D:] by A2, A3, FUNCT_2:29;
A7: J * K = id (product (E ^ <*D*>)) by A2, A3, FUNCT_2:29;

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

let z1, z2 be object ; :: thesis: ( z1 in Funcs (D,(Funcs ((product E),F))) & z2 in Funcs (D,(Funcs ((product E),F))) & L . z1 = L . z2 implies z1 = z2 )
assume A8: ( z1 in Funcs (D,(Funcs ((product E),F))) & z2 in Funcs (D,(Funcs ((product E),F))) & L . z1 = L . z2 ) ; :: thesis: z1 = z2
(I . z1) * K = L . z2 by A5, A8;
then A9: ((I . z1) * K) * J = ((I . z2) * K) * J by A5, A8;
(I . z1) * (K * J) = ((I . z1) * K) * J by RELAT_1:36;
then A10: (I . z1) * (K * J) = (I . z2) * (K * J) by A9, RELAT_1:36;
( I . z1 is Function of [:(product E),D:],F & I . z2 is Function of [:(product E),D:],F ) by A8, FUNCT_2:5, FUNCT_2:66;
then ( (I . z1) * (K * J) = I . z1 & (I . z2) * (K * J) = I . z2 ) by A6, FUNCT_2:17;
hence z1 = z2 by A1, FUNCT_2:19, A8, A10; :: thesis: verum

end;

then A11: 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),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
A12: ( zf in Funcs (D,(Funcs ((product E),F))) & I . zf = wf * J ) by FUNCT_2:11;
L . zf = (wf * J) * K by A5, A12;
then L . zf = wf * (id (product (E ^ <*D*>))) by A7, RELAT_1:36;
then L . zf = w by FUNCT_2:17;
hence w in rng L by A12, FUNCT_2:112; :: thesis: verum

end;

then Funcs ((product (E ^ <*D*>)),F) c= rng L by TARSKI:def 3;
then L is onto by FUNCT_2:def 3, XBOOLE_0:def 10;
hence L is bijective by A11; :: thesis: for f being Function of D,(Funcs ((product E),F))
for e being FinSequence
for d being object st e in product E & d in D holds
(L . f) . (e ^ <*d*>) = (f . d) . e
thus for f being Function of D,(Funcs ((product E),F))
for e being FinSequence
for d being object st e in product E & d in D holds
(L . f) . (e ^ <*d*>) = (f . d) . e :: thesis: verum

proof

let f be Function of D,(Funcs ((product E),F)); :: thesis: for e being FinSequence
for d being object st e in product E & d in D holds
(L . f) . (e ^ <*d*>) = (f . d) . e
let e be FinSequence; :: thesis: for d being object st e in product E & d in D holds
(L . f) . (e ^ <*d*>) = (f . d) . e
let d be object ; :: thesis: ( e in product E & d in D implies (L . f) . (e ^ <*d*>) = (f . d) . e )
assume A13: ( e in product E & d in D ) ; :: thesis: (L . f) . (e ^ <*d*>) = (f . d) . e
then A14: (I . f) . (e,d) = (f . d) . e by A1;
A15: J . (e,d) = e ^ <*d*> by A2, A13;
[e,d] in [:(product E),D:] by A13, ZFMISC_1:def 2;
then A16: ( J . (e,d) in product (E ^ <*D*>) & K . (J . (e,d)) = [e,d] ) by A2, FUNCT_2:5, FUNCT_2:26;
f in Funcs (D,(Funcs ((product E),F))) by FUNCT_2:8;
then (L . f) . (e ^ <*d*>) = ((I . f) * K) . (J . (e,d)) by A15, A5;
hence (L . f) . (e ^ <*d*>) = (f . d) . e by A14, A16, FUNCT_2:15; :: thesis: verum

end;