let f be Function; :: thesis: for x1, x2, y1, y2 being set st x1 in dom f & y1 in f . x1 & x2 in dom f & y2 in f . x2 holds
(x1,x2) --> (y1,y2) in sproduct f
let x1, x2, y1, y2 be set ; :: thesis: ( x1 in dom f & y1 in f . x1 & x2 in dom f & y2 in f . x2 implies (x1,x2) --> (y1,y2) in sproduct f )
assume that
A1: x1 in dom f and
A2: y1 in f . x1 ; :: thesis: ( not x2 in dom f or not y2 in f . x2 or (x1,x2) --> (y1,y2) in sproduct f )
A3: x1 .--> y1 in sproduct f by A1, A2, Th60;
assume that
A4: x2 in dom f and
A5: y2 in f . x2 ; :: thesis: (x1,x2) --> (y1,y2) in sproduct f
A6: x2 .--> y2 in sproduct f by A4, A5, Th60;
(x1,x2) --> (y1,y2) = (x1 .--> y1) +* (x2 .--> y2) by FUNCT_4:def 4;
hence (x1,x2) --> (y1,y2) in sproduct f by A3, A6, Th70; :: thesis: verum