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] A7: for x being Element of X holds S₁[{.x.}] 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