let f be Function; for A, B being set
for i, j being object st i in dom f & j in dom f & A c= f . i & B c= f . j holds
product (f +* ((i,j) --> (A,B))) c= product f
let A, B be set ; for i, j being object st i in dom f & j in dom f & A c= f . i & B c= f . j holds
product (f +* ((i,j) --> (A,B))) c= product f
let i, j be object ; ( i in dom f & j in dom f & A c= f . i & B c= f . j implies product (f +* ((i,j) --> (A,B))) c= product f )
assume A1:
( i in dom f & j in dom f & A c= f . i & B c= f . j )
; product (f +* ((i,j) --> (A,B))) c= product f
then
product f = product (f +* ((i,j) --> ((f . i),(f . j))))
by Th11;
hence
product (f +* ((i,j) --> (A,B))) c= product f
by A1, Th31; verum