let D1, D2, D be non empty set ; 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; 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 ; 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; 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; 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 ; ( x in A implies ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x)) )
assume A3:
x in A
; ((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; verum