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 ( x1 in dom f & y1 in f . x1 ) ; :: thesis: ( not x2 in dom f or not y2 in f . x2 or x1,x2 --> y1,y2 in sproduct f )
then A1: x1 .--> y1 in sproduct f by Th76;
assume ( x2 in dom f & y2 in f . x2 ) ; :: thesis: x1,x2 --> y1,y2 in sproduct f
then A2: x2 .--> y2 in sproduct f by Th76;
x1,x2 --> y1,y2 = (x1 .--> y1) +* (x2 .--> y2) by FUNCT_4:def 4;
hence x1,x2 --> y1,y2 in sproduct f by A1, A2, Th86; :: thesis: verum