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

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