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]
A7: B1 c= X by FINSUB_1:def 5;
A8: B2 c= X by FINSUB_1:def 5;
thus F $$ ((f .: (B1 \/ B2)),g) = F $$ (((f .: B1) \/ (f .: B2)),g) by RELAT_1:120
.= F . ((F $$ ((f .: B1),g)),(F $$ ((f .: B2),g))) by A1, A2, A7, A8, Th18, A4
.= F $$ ((B1 \/ B2),(g * f)) by A1, A2, A6, Th18 ; :: 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:59
.= g . (f . x) by A2, Th14
.= (g * f) . x by FUNCT_2:15
.= F $$ ({.x.},(g * f)) by A2, Th14 ;
:: 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