let DX1, DX2 be non empty set ; :: thesis: for F1 being Function of DX1,REAL
for F2 being Function of DX2,REAL
for G being Function of [:DX1,DX2:],REAL
for Y1 being non empty finite Subset of DX1
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . x,y = (F1 . x) * (F2 . y) ) holds
setopfunc Y3,[:DX1,DX2:],REAL ,G,addreal = (setopfunc Y1,DX1,REAL ,F1,addreal ) * (setopfunc Y2,DX2,REAL ,F2,addreal )
let F1 be Function of DX1,REAL ; :: thesis: for F2 being Function of DX2,REAL
for G being Function of [:DX1,DX2:],REAL
for Y1 being non empty finite Subset of DX1
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . x,y = (F1 . x) * (F2 . y) ) holds
setopfunc Y3,[:DX1,DX2:],REAL ,G,addreal = (setopfunc Y1,DX1,REAL ,F1,addreal ) * (setopfunc Y2,DX2,REAL ,F2,addreal )
let F2 be Function of DX2,REAL ; :: thesis: for G being Function of [:DX1,DX2:],REAL
for Y1 being non empty finite Subset of DX1
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . x,y = (F1 . x) * (F2 . y) ) holds
setopfunc Y3,[:DX1,DX2:],REAL ,G,addreal = (setopfunc Y1,DX1,REAL ,F1,addreal ) * (setopfunc Y2,DX2,REAL ,F2,addreal )
let G be Function of [:DX1,DX2:],REAL ; :: thesis: for Y1 being non empty finite Subset of DX1
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . x,y = (F1 . x) * (F2 . y) ) holds
setopfunc Y3,[:DX1,DX2:],REAL ,G,addreal = (setopfunc Y1,DX1,REAL ,F1,addreal ) * (setopfunc Y2,DX2,REAL ,F2,addreal )
let Y1 be non empty finite Subset of DX1; :: thesis: for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . x,y = (F1 . x) * (F2 . y) ) holds
setopfunc Y3,[:DX1,DX2:],REAL ,G,addreal = (setopfunc Y1,DX1,REAL ,F1,addreal ) * (setopfunc Y2,DX2,REAL ,F2,addreal )
let Y2 be non empty finite Subset of DX2; :: thesis: for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . x,y = (F1 . x) * (F2 . y) ) holds
setopfunc Y3,[:DX1,DX2:],REAL ,G,addreal = (setopfunc Y1,DX1,REAL ,F1,addreal ) * (setopfunc Y2,DX2,REAL ,F2,addreal )
let Y3 be finite Subset of [:DX1,DX2:]; :: thesis: ( Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . x,y = (F1 . x) * (F2 . y) ) implies setopfunc Y3,[:DX1,DX2:],REAL ,G,addreal = (setopfunc Y1,DX1,REAL ,F1,addreal ) * (setopfunc Y2,DX2,REAL ,F2,addreal ) )
assume AS: ( Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . x,y = (F1 . x) * (F2 . y) ) ) ; :: thesis: setopfunc Y3,[:DX1,DX2:],REAL ,G,addreal = (setopfunc Y1,DX1,REAL ,F1,addreal ) * (setopfunc Y2,DX2,REAL ,F2,addreal )
consider p1 being FinSequence of DX1 such that
Q1: ( p1 is one-to-one & rng p1 = Y1 & setopfunc Y1,DX1,REAL ,F1,addreal = Sum (Func_Seq F1,p1) ) by LMXY092;
consider p2 being FinSequence of DX2 such that
Q2: ( p2 is one-to-one & rng p2 = Y2 & setopfunc Y2,DX2,REAL ,F2,addreal = Sum (Func_Seq F2,p2) ) by LMXY092;
consider p3 being FinSequence of [:DX1,DX2:] such that
Q3: ( p3 is one-to-one & rng p3 = Y3 & setopfunc Y3,[:DX1,DX2:],REAL ,G,addreal = Sum (Func_Seq G,p3) ) by LMXY092;
thus setopfunc Y3,[:DX1,DX2:],REAL ,G,addreal = (setopfunc Y1,DX1,REAL ,F1,addreal ) * (setopfunc Y2,DX2,REAL ,F2,addreal ) by AS, Q1, Q2, Q3, LMXY090A; :: thesis: verum