let C, D1, D2 be non empty set ; 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; 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; for c being Element of C holds <:f1,f2:> . c = [(f1 . c),(f2 . c)]
let c be Element of C; <:f1,f2:> . c = [(f1 . c),(f2 . c)]
( dom f1 = C & dom f2 = C )
by FUNCT_2:def 1;
hence
<:f1,f2:> . c = [(f1 . c),(f2 . c)]
by Th49; verum