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 that
A1: F is idempotent and
A2: ( 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 A3: 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)
defpred S₁[ Element of Fin X] means F $$ (f .: $1),g = F $$ $1,(g * f);
A4: dom f = X by FUNCT_2:def 1;
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: ( F $$ (f .: B1),g = F $$ B1,(g * f) & F $$ (f .: B2),g = F $$ B2,(g * f) ) ; :: thesis: S₁[B1 \/ B2]
B1 c= X by FINSUB_1:def 5;
then X /\ B1 <> {} by XBOOLE_1:28;
then X meets B1 by XBOOLE_0:def 7;
then A7: f .: B1 <> {} by A4, RELAT_1:151;
B2 c= X by FINSUB_1:def 5;
then X /\ B2 <> {} by XBOOLE_1:28;
then X meets B2 by XBOOLE_0:def 7;
then A8: f .: B2 <> {} by A4, RELAT_1:151;
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, A2, A7, A8, Th30
.= F $$ (B1 \/ B2),(g * f) by A1, A2, A6, Th30 ; :: thesis: verum

end;

A9: 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 A4, FUNCT_1:117
.= g . (f . x) by A2, Th26
.= (g * f) . x by FUNCT_2:21
.= F $$ {.x.},(g * f) by A2, Th26 ;
:: thesis: verum

end;

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