let f be Function; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum