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 A3, A1, FUNCOP_1:22, FUNCT_2:def 1;

hence ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x)) by A3, A1, A2, FUNCT_5:38; :: thesis: verum

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 A3, A1, FUNCOP_1:22, FUNCT_2:def 1;

hence ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x)) by A3, A1, A2, FUNCT_5:38; :: thesis: verum