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*> )
( ( [(f1 . x),(f2 . y)] = [y1,y2] implies ( f1 . x = y1 & f2 . y = y2 ) ) & ( f1 . x = y1 & f2 . y = y2 implies [(f1 . x),(f2 . y)] = [y1,y2] ) & <*(f1 . x),(f2 . y)*> . 1 = f1 . x & <*(f1 . x),(f2 . y)*> . 2 = f2 . y & <*y1,y2*> . 1 = y1 & <*y1,y2*> . 2 = y2 ) by FINSEQ_1:61, ZFMISC_1:33;
hence ( [:f1,f2:] . x,y = [y1,y2] iff (Frege <*f1,f2*>) . <*x,y*> = <*y1,y2*> ) by A1, Th65, FUNCT_3:def 9; :: thesis: verum