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, Th76;
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, Th76;
x1,x2 --> y1,y2 = (x1 .--> y1) +* (x2 .--> y2) by FUNCT_4:def 4;
hence x1,x2 --> y1,y2 in sproduct f by A3, A6, Th86; :: thesis: verum