let X, Y 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, Th18
.= F . ((F $$ (B1,(G [:] (f,a)))),(F $$ (B2,(G [:] (f,a))))) by A3, A6, BINOP_1:11
.= F $$ ((B1 \/ B2),(G [:] (f,a))) by A1, A2, Th18 ; :: 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, Th14
.= (G [:] (f,a)) . x by FUNCOP_1:48
.= F $$ ({.x.},(G [:] (f,a))) by A2, Th14 ; :: 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