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 . (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, Th18
.= F . ((F $$ (B1,(G [;] (a,f)))),(F $$ (B2,(G [;] (a,f))))) by A3, A6, BINOP_1:11
.= F $$ ((B1 \/ B2),(G [;] (a,f))) 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 . (a,(F $$ ({.x.},f))) = G . (a,(f . x)) by A2, Th14
.= (G [;] (a,f)) . x by FUNCOP_1:53
.= F $$ ({.x.},(G [;] (a,f))) 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 . (a,(F $$ (B,f))) = F $$ (B,(G [;] (a,f))) by A4; :: thesis: verum