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