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:28, FUNCT_2:def 1;
hence
(f,D .: A) .. f1,f2,x = f . (f1 . x),(f2 . x)
by A3, A1, A2, FUNCT_5:45; verum