let C1, D1, C2, D2 be non empty set ; :: thesis: for f1 being Function of C1,D1
for f2 being Function of C2,D2
for c1 being Element of C1
for c2 being Element of C2 holds [:f1,f2:] . c1,c2 = [(f1 . c1),(f2 . c2)]
let f1 be Function of C1,D1; :: thesis: for f2 being Function of C2,D2
for c1 being Element of C1
for c2 being Element of C2 holds [:f1,f2:] . c1,c2 = [(f1 . c1),(f2 . c2)]
let f2 be Function of C2,D2; :: thesis: for c1 being Element of C1
for c2 being Element of C2 holds [:f1,f2:] . c1,c2 = [(f1 . c1),(f2 . c2)]
let c1 be Element of C1; :: thesis: for c2 being Element of C2 holds [:f1,f2:] . c1,c2 = [(f1 . c1),(f2 . c2)]
let c2 be Element of C2; :: thesis: [:f1,f2:] . c1,c2 = [(f1 . c1),(f2 . c2)]
( c1 in C1 & c2 in C2 & dom f1 = C1 & dom f2 = C2 ) by FUNCT_2:def 1;
hence [:f1,f2:] . c1,c2 = [(f1 . c1),(f2 . c2)] by Def9; :: thesis: verum