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 . (F $$ B,f),a = F $$ B,(G [:] f,a)
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 . (F $$ B,f),a = F $$ B,(G [:] f,a) )
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 . (F $$ B,f),a = F $$ B,(G [:] f,a)
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 . (F $$ B,f),a = F $$ B,(G [:] f,a) )
assume A4: B <> {} ; :: thesis: for f being Function of X,Y
for a being Element of Y holds G . (F $$ B,f),a = F $$ B,(G [:] f,a)
let f be Function of X,Y; :: thesis: for a being Element of Y holds G . (F $$ B,f),a = F $$ B,(G [:] f,a)
let a be Element of Y; :: thesis: G . (F $$ B,f),a = F $$ B,(G [:] f,a)
defpred S₁[ Element of Fin X] means G . (F $$ $1,f),a = F $$ $1,(G [:] f,a);
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 . (F $$ B1,f),a = F $$ B1,(G [:] f,a) & G . (F $$ B2,f),a = F $$ B2,(G [:] f,a) ) ; :: thesis: S₁[B1 \/ B2]
thus G . (F $$ (B1 \/ B2),f),a = G . (F . (F $$ B1,f),(F $$ B2,f)),a by A1, A2, Th30
.= F . (F $$ B1,(G [:] f,a)),(F $$ B2,(G [:] f,a)) by A3, A6, BINOP_1:23
.= F $$ (B1 \/ B2),(G [:] f,a) 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 . (F $$ {.x.},f),a = G . (f . x),a by A2, Th26
.= (G [:] f,a) . x by FUNCOP_1:60
.= F $$ {.x.},(G [:] f,a) 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 . (F $$ B,f),a = F $$ B,(G [:] f,a) by A4; :: thesis: verum