let X, Y be non empty set ; :: thesis: for F being BinOp of Y st F is commutative & F is associative & F is idempotent holds
for Z being non empty set
for G being BinOp of Z st G is commutative & G is associative & G is idempotent holds
for f being Function of X,Y
for g being Function of Y,Z st ( for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ) holds
for B being Element of Fin X st B <> {} holds
g . (F $$ (B,f)) = G $$ (B,(g * f))
let F be BinOp of Y; :: thesis: ( F is commutative & F is associative & F is idempotent implies for Z being non empty set
for G being BinOp of Z st G is commutative & G is associative & G is idempotent holds
for f being Function of X,Y
for g being Function of Y,Z st ( for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ) holds
for B being Element of Fin X st B <> {} holds
g . (F $$ (B,f)) = G $$ (B,(g * f)) )
assume that
A1: ( F is commutative & F is associative ) and
A2: F is idempotent ; :: thesis: for Z being non empty set
for G being BinOp of Z st G is commutative & G is associative & G is idempotent holds
for f being Function of X,Y
for g being Function of Y,Z st ( for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ) holds
for B being Element of Fin X st B <> {} holds
g . (F $$ (B,f)) = G $$ (B,(g * f))
let Z be non empty set ; :: thesis: for G being BinOp of Z st G is commutative & G is associative & G is idempotent holds
for f being Function of X,Y
for g being Function of Y,Z st ( for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ) holds
for B being Element of Fin X st B <> {} holds
g . (F $$ (B,f)) = G $$ (B,(g * f))
let G be BinOp of Z; :: thesis: ( G is commutative & G is associative & G is idempotent implies for f being Function of X,Y
for g being Function of Y,Z st ( for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ) holds
for B being Element of Fin X st B <> {} holds
g . (F $$ (B,f)) = G $$ (B,(g * f)) )
assume that
A3: ( G is commutative & G is associative ) and
A4: G is idempotent ; :: thesis: for f being Function of X,Y
for g being Function of Y,Z st ( for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ) holds
for B being Element of Fin X st B <> {} holds
g . (F $$ (B,f)) = G $$ (B,(g * f))
let f be Function of X,Y; :: thesis: for g being Function of Y,Z st ( for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ) holds
for B being Element of Fin X st B <> {} holds
g . (F $$ (B,f)) = G $$ (B,(g * f))
let g be Function of Y,Z; :: thesis: ( ( for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ) implies for B being Element of Fin X st B <> {} holds
g . (F $$ (B,f)) = G $$ (B,(g * f)) )
assume A5: for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ; :: thesis: for B being Element of Fin X st B <> {} holds
g . (F $$ (B,f)) = G $$ (B,(g * f))
defpred S₁[ Element of Fin X] means ( $1 <> {} implies g . (F $$ ($1,f)) = G $$ ($1,(g * f)) );
A6: for B9 being Element of Fin X
for b being Element of X st S₁[B9] holds
S₁[B9 \/ {.b.}]

proof

let B be Element of Fin X; :: thesis: for b being Element of X st S₁[B] holds
S₁[B \/ {.b.}]
let x be Element of X; :: thesis: ( S₁[B] implies S₁[B \/ {.x.}] )
assume that
A7: ( B <> {} implies g . (F $$ (B,f)) = G $$ (B,(g * f)) ) and
B \/ {x} <> {} ; :: thesis: g . (F $$ ((B \/ {.x.}),f)) = G $$ ((B \/ {.x.}),(g * f))

per cases ( B = {} or B <> {} ) ;

suppose A8: B = {} ; :: thesis: g . (F $$ ((B \/ {.x.}),f)) = G $$ ((B \/ {.x.}),(g * f))

hence g . (F $$ ((B \/ {.x.}),f)) = g . (f . x) by A1, Th14
.= (g * f) . x by FUNCT_2:15
.= G $$ ((B \/ {.x.}),(g * f)) by A3, A8, Th14 ;
:: thesis: verum

end;

suppose A9: B <> {} ; :: thesis: g . (F $$ ((B \/ {.x.}),f)) = G $$ ((B \/ {.x.}),(g * f))

hence g . (F $$ ((B \/ {.x.}),f)) = g . (F . ((F $$ (B,f)),(f . x))) by A1, A2, Th17
.= G . ((g . (F $$ (B,f))),(g . (f . x))) by A5
.= G . ((G $$ (B,(g * f))),((g * f) . x)) by A7, A9, FUNCT_2:15
.= G $$ ((B \/ {.x.}),(g * f)) by A3, A4, A9, Th17 ;
:: thesis: verum

end;

end;

end;

A10: S₁[ {}. X] ;
thus for B being Element of Fin X holds S₁[B] from SETWISEO:sch 4(A10, A6); :: thesis: verum