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