let Y, X be non empty set ; :: thesis: for F, G being BinOp of Y st F is idempotent & F is commutative & F is associative & G is_distributive_wrt F holds
for B being Element of Fin X st B <> {} holds
for f being Function of X,Y
for a being Element of Y holds G . a,(F $$ B,f) = F $$ B,(G [;] a,f)
let F, G be BinOp of Y; :: thesis: ( F is idempotent & F is commutative & F is associative & G is_distributive_wrt F implies for B being Element of Fin X st B <> {} holds
for f being Function of X,Y
for a being Element of Y holds G . a,(F $$ B,f) = F $$ B,(G [;] a,f) )
assume that
A1: F is idempotent and
A2: ( F is commutative & F is associative ) and
A3: G is_distributive_wrt F ; :: thesis: for B being Element of Fin X st B <> {} holds
for f being Function of X,Y
for a being Element of Y holds G . a,(F $$ B,f) = F $$ B,(G [;] a,f)
let B be Element of Fin X; :: thesis: ( B <> {} implies for f being Function of X,Y
for a being Element of Y holds G . a,(F $$ B,f) = F $$ B,(G [;] a,f) )
assume A4: B <> {} ; :: thesis: for f being Function of X,Y
for a being Element of Y holds G . a,(F $$ B,f) = F $$ B,(G [;] a,f)
let f be Function of X,Y; :: thesis: for a being Element of Y holds G . a,(F $$ B,f) = F $$ B,(G [;] a,f)
let a be Element of Y; :: thesis: G . a,(F $$ B,f) = F $$ B,(G [;] a,f)
defpred S₁[ Element of Fin X] means G . a,(F $$ $1,f) = F $$ $1,(G [;] a,f);
A5: for B1, B2 being non empty Element of Fin X st S₁[B1] & S₁[B2] holds
S₁[B1 \/ B2]

proof

let B1, B2 be non empty Element of Fin X; :: thesis: ( S₁[B1] & S₁[B2] implies S₁[B1 \/ B2] )
assume A6: ( G . a,(F $$ B1,f) = F $$ B1,(G [;] a,f) & G . a,(F $$ B2,f) = F $$ B2,(G [;] a,f) ) ; :: thesis: S₁[B1 \/ B2]
thus G . a,(F $$ (B1 \/ B2),f) = G . a,(F . (F $$ B1,f),(F $$ B2,f)) by A1, A2, Th30
.= F . (F $$ B1,(G [;] a,f)),(F $$ B2,(G [;] a,f)) by A3, A6, BINOP_1:23
.= F $$ (B1 \/ B2),(G [;] a,f) by A1, A2, Th30 ; :: thesis: verum

end;

A7: for x being Element of X holds S₁[{.x.}]

proof

let x be Element of X; :: thesis: S₁[{.x.}]
thus G . a,(F $$ {.x.},f) = G . a,(f . x) by A2, Th26
.= (G [;] a,f) . x by FUNCOP_1:66
.= F $$ {.x.},(G [;] a,f) by A2, Th26 ; :: thesis: verum

end;

for B being non empty Element of Fin X holds S₁[B] from SETWISEO:sch 3(A7, A5);
hence G . a,(F $$ B,f) = F $$ B,(G [;] a,f) by A4; :: thesis: verum