let D1, D2, D be non empty set ; :: thesis: for f being Function of [:D1,D2:],D
for A being set
for f1 being Function of A,D1
for f2 being Function of A,D2
for x being set st x in A holds
((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x))

let f be Function of [:D1,D2:],D; :: thesis: for A being set
for f1 being Function of A,D1
for f2 being Function of A,D2
for x being set st x in A holds
((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x))

let A be set ; :: thesis: for f1 being Function of A,D1
for f2 being Function of A,D2
for x being set st x in A holds
((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x))

let f1 be Function of A,D1; :: thesis: for f2 being Function of A,D2
for x being set st x in A holds
((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x))

let f2 be Function of A,D2; :: thesis: for x being set st x in A holds
((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x))

( dom f2 = A & rng f2 c= D2 ) by FUNCT_2:def 1;
then reconsider f2 = f2 as Element of Funcs (A,D2) by FUNCT_2:def 2;
( dom f1 = A & rng f1 c= D1 ) by FUNCT_2:def 1;
then reconsider f1 = f1 as Element of Funcs (A,D1) by FUNCT_2:def 2;
A1: dom (f .: (f1,f2)) = A by FUNCT_2:def 1;
A2: ( ((f,D) .: A) . (f1,f2) = f .: (f1,f2) & [f1,f2] = [f1,f2] ) by Def2;
let x be set ; :: thesis: ( x in A implies ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x)) )
assume A3: x in A ; :: thesis: ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x))
( dom ((f,D) .: A) = [:(Funcs (A,D1)),(Funcs (A,D2)):] & (f .: (f1,f2)) . x = f . ((f1 . x),(f2 . x)) ) by ;
hence ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x)) by ; :: thesis: verum