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 A1: ( 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
A2: ( p1 is one-to-one & rng p1 = Y1 & setopfunc (Y1,DX1,REAL,F1,addreal) = Sum (Func_Seq (F1,p1)) ) by Th9;
consider p2 being FinSequence of DX2 such that
A3: ( p2 is one-to-one & rng p2 = Y2 & setopfunc (Y2,DX2,REAL,F2,addreal) = Sum (Func_Seq (F2,p2)) ) by Th9;
consider p3 being FinSequence of [:DX1,DX2:] such that
A4: ( p3 is one-to-one & rng p3 = Y3 & setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = Sum (Func_Seq (G,p3)) ) by Th9;
thus setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = (setopfunc (Y1,DX1,REAL,F1,addreal)) * (setopfunc (Y2,DX2,REAL,F2,addreal)) by A1, A2, A3, A4, Th11; :: thesis: verum