let C, D1, D2 be non empty set ; :: thesis: for f1 being Function of C,D1
for f2 being Function of C,D2
for c being Element of C holds <:f1,f2:> . c = [(f1 . c),(f2 . c)]
let f1 be Function of C,D1; :: thesis: for f2 being Function of C,D2
for c being Element of C holds <:f1,f2:> . c = [(f1 . c),(f2 . c)]
let f2 be Function of C,D2; :: thesis: for c being Element of C holds <:f1,f2:> . c = [(f1 . c),(f2 . c)]
let c be Element of C; :: thesis: <:f1,f2:> . c = [(f1 . c),(f2 . c)]
( c in C & dom f1 = C & dom f2 = C ) by FUNCT_2:def 1;
hence <:f1,f2:> . c = [(f1 . c),(f2 . c)] by Th69; :: thesis: verum