let x be set ; :: thesis: for f1, f2 being Function st x in dom f1 & x in dom f2 holds
for y1, y2 being set holds
( <:f1,f2:> . x = [y1,y2] iff <:<*f1,f2*>:> . x = <*y1,y2*> )
let f1, f2 be Function; :: thesis: ( x in dom f1 & x in dom f2 implies for y1, y2 being set holds
( <:f1,f2:> . x = [y1,y2] iff <:<*f1,f2*>:> . x = <*y1,y2*> ) )
A1: ( <*(f1 . x),(f2 . x)*> . 1 = f1 . x & <*(f1 . x),(f2 . x)*> . 2 = f2 . x ) by FINSEQ_1:61;
assume ( x in dom f1 & x in dom f2 ) ; :: thesis: for y1, y2 being set holds
( <:f1,f2:> . x = [y1,y2] iff <:<*f1,f2*>:> . x = <*y1,y2*> )
then A2: x in (dom f1) /\ (dom f2) by XBOOLE_0:def 4;
let y1, y2 be set ; :: thesis: ( <:f1,f2:> . x = [y1,y2] iff <:<*f1,f2*>:> . x = <*y1,y2*> )
A3: ( <*y1,y2*> . 1 = y1 & <*y1,y2*> . 2 = y2 ) by FINSEQ_1:61;
( [(f1 . x),(f2 . x)] = [y1,y2] iff ( f1 . x = y1 & f2 . x = y2 ) ) by ZFMISC_1:33;
hence ( <:f1,f2:> . x = [y1,y2] iff <:<*f1,f2*>:> . x = <*y1,y2*> ) by A2, A1, A3, Th62, FUNCT_3:68; :: thesis: verum