let A, X, Y be non empty set ; :: thesis: for F being BinOp of A st F is idempotent & F is commutative & F is associative holds
for B being Element of Fin X st B <> {} holds
for f being Function of X,Y
for g being Function of Y,A holds F $$ (f .: B),g = F $$ B,(g * f)
let F be BinOp of A; :: thesis: ( F is idempotent & F is commutative & F is associative implies for B being Element of Fin X st B <> {} holds
for f being Function of X,Y
for g being Function of Y,A holds F $$ (f .: B),g = F $$ B,(g * f) )
assume A1: ( F is idempotent & F is commutative & F is associative ) ; :: thesis: for B being Element of Fin X st B <> {} holds
for f being Function of X,Y
for g being Function of Y,A holds F $$ (f .: B),g = F $$ B,(g * f)
let B be Element of Fin X; :: thesis: ( B <> {} implies for f being Function of X,Y
for g being Function of Y,A holds F $$ (f .: B),g = F $$ B,(g * f) )
assume A2: B <> {} ; :: thesis: for f being Function of X,Y
for g being Function of Y,A holds F $$ (f .: B),g = F $$ B,(g * f)
let f be Function of X,Y; :: thesis: for g being Function of Y,A holds F $$ (f .: B),g = F $$ B,(g * f)
let g be Function of Y,A; :: thesis: F $$ (f .: B),g = F $$ B,(g * f)
A3: dom f = X by FUNCT_2:def 1;
defpred S₁[ Element of Fin X] means F $$ (f .: $1),g = F $$ $1,(g * f);
A4: for x being Element of X holds S₁[{.x.}]

proof

let x be Element of X; :: thesis: S₁[{.x.}]
f .: {.x.} = Im f,x ;
hence F $$ (f .: {.x.}),g = F $$ {.(f . x).},g by A3, FUNCT_1:117
.= g . (f . x) by A1, Th26
.= (g * f) . x by FUNCT_2:21
.= F $$ {.x.},(g * f) by A1, Th26 ;
:: thesis: verum

end;

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] )
( B1 c= X & B2 c= X ) by FINSUB_1:def 5;
then ( X /\ B1 <> {} & X /\ B2 <> {} ) by XBOOLE_1:28;
then ( X meets B1 & X meets B2 ) by XBOOLE_0:def 7;
then A7: ( f .: B1 <> {} & f .: B2 <> {} ) by A3, RELAT_1:151;
assume A8: ( F $$ (f .: B1),g = F $$ B1,(g * f) & F $$ (f .: B2),g = F $$ B2,(g * f) ) ; :: thesis: S₁[B1 \/ B2]
thus F $$ (f .: (B1 \/ B2)),g = F $$ ((f .: B1) \/ (f .: B2)),g by RELAT_1:153
.= F . (F $$ (f .: B1),g),(F $$ (f .: B2),g) by A1, A7, Th30
.= F $$ (B1 \/ B2),(g * f) by A1, A8, Th30 ; :: thesis: verum

end;

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