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 f, g being Function of X,Y
for A, B being Element of Fin X st A <> {} & f .: A = g .: B holds
F $$ (A,f) = F $$ (B,g)
let F be BinOp of Y; :: thesis: ( F is commutative & F is associative & F is idempotent implies for f, g being Function of X,Y
for A, B being Element of Fin X st A <> {} & f .: A = g .: B holds
F $$ (A,f) = F $$ (B,g) )
assume that
A1: F is commutative and
A2: F is associative and
A3: F is idempotent ; :: thesis: for f, g being Function of X,Y
for A, B being Element of Fin X st A <> {} & f .: A = g .: B holds
F $$ (A,f) = F $$ (B,g)
let f, g be Function of X,Y; :: thesis: for A, B being Element of Fin X st A <> {} & f .: A = g .: B holds
F $$ (A,f) = F $$ (B,g)
defpred S₁[ Element of Fin X] means ( $1 <> {} implies for B being Element of Fin X st f .: $1 = g .: B holds
F $$ ($1,f) = F $$ (B,g) );
A4: for B9 being Element of Fin X
for b being Element of X st S₁[B9] holds
S₁[B9 \/ {.b.}]

proof

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

per cases ( f . x in f .: A or not f . x in f .: A ) ;

suppose f . x in f .: A ; :: thesis: F $$ ((A \/ {.x.}),f) = F $$ (B,g)

then consider x9 being Element of X such that
A7: x9 in A and
A8: f . x9 = f . x by FUNCT_2:65;
A9: g .: B = (f .: A) \/ (Im (f,x)) by A6, RELAT_1:120
.= (f .: A) \/ {(f . x)} by Th5
.= f .: A by A7, A8, FUNCT_2:35, ZFMISC_1:40 ;
thus F $$ ((A \/ {.x.}),f) = F . ((F $$ (A,f)),(f . x)) by A1, A2, A3, A7, Th17
.= F . ((F $$ ((A \/ {.x9.}),f)),(f . x)) by A7, ZFMISC_1:40
.= F . ((F . ((F $$ (A,f)),(f . x9))),(f . x)) by A1, A2, A3, A7, Th17
.= F . ((F $$ (A,f)),(F . ((f . x9),(f . x9)))) by A2, A8
.= F $$ ((A \/ {.x9.}),f) by A1, A2, A3, A7, Th17
.= F $$ (A,f) by A7, ZFMISC_1:40
.= F $$ (B,g) by A5, A7, A9 ; :: thesis: verum

end;

suppose A10: not f . x in f .: A ; :: thesis: F $$ ((A \/ {.x.}),f) = F $$ (B,g)

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

suppose A11: A = {} ; :: thesis: F $$ ((A \/ {.x.}),f) = F $$ (B,g)

then A12: g .: B = Im (f,x) by A6
.= {(f . x)} by Th5 ;
thus F $$ ((A \/ {.x.}),f) = f . x by A1, A2, A11, Th14
.= F $$ (B,g) by A1, A2, A3, A12, Th22 ; :: thesis: verum

end;

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

reconsider B1 = B \ (g " {(f . x)}) as Element of Fin X by Th8;

A14: now :: thesis: not B1 = {}

assume B1 = {} ; :: thesis: contradiction
then A15: g .: B c= g .: (g " {(f . x)}) by RELAT_1:123, XBOOLE_1:37;
g .: (g " {(f . x)}) c= {(f . x)} by FUNCT_1:75;
then f .: (A \/ {x}) c= {(f . x)} by A6, A15;
then (f .: A) \/ (f .: {x}) c= {(f . x)} by RELAT_1:120;
then f .: A = (f .: A) /\ {(f . x)} by XBOOLE_1:11, XBOOLE_1:28
.= {} by A10, XBOOLE_0:def 7, ZFMISC_1:50 ;
hence contradiction by A13, Th10; :: thesis: verum

end;

reconsider B2 = B /\ (g " {(f . x)}) as Element of Fin X by Th8, XBOOLE_1:17;
A16: B = B1 \/ B2 by XBOOLE_1:51;
A17: for b being Element of X st b in B2 holds
g . b = f . x

proof

let b be Element of X; :: thesis: ( b in B2 implies g . b = f . x )
assume b in B2 ; :: thesis: g . b = f . x
then b in g " {(f . x)} by XBOOLE_0:def 4;
then g . b in {(f . x)} by FUNCT_1:def 7;
hence g . b = f . x by TARSKI:def 1; :: thesis: verum

end;

A18: f .: A = (f .: A) \ {(f . x)} by A10, ZFMISC_1:57
.= (f .: A) \ (Im (f,x)) by Th5
.= ((f .: A) \/ (f .: {x})) \ (f .: {x}) by XBOOLE_1:40
.= (f .: (A \/ {x})) \ (Im (f,x)) by RELAT_1:120
.= (g .: B) \ {(f . x)} by A6, Th5
.= g .: B1 by Th3 ;
x in A \/ {x} by ZFMISC_1:136;
then consider x9 being Element of X such that
A19: x9 in B and
A20: g . x9 = f . x by A6, FUNCT_2:35, FUNCT_2:65;
x9 in g " {(f . x)} by A20, Th4;
then A21: B2 <> {} by A19, XBOOLE_0:def 4;
thus F $$ ((A \/ {.x.}),f) = F . ((F $$ (A,f)),(f . x)) by A1, A2, A3, A13, Th17
.= F . ((F $$ (B1,g)),(f . x)) by A5, A13, A18
.= F . ((F $$ (B1,g)),(F $$ (B2,g))) by A1, A2, A3, A21, A17, Th21
.= F $$ (B,g) by A1, A2, A3, A16, A14, A21, Th18 ; :: thesis: verum

end;

end;

end;

end;

end;

A22: S₁[ {}. X] ;
A23: for A being Element of Fin X holds S₁[A] from SETWISEO:sch 4(A22, A4);
let A, B be Element of Fin X; :: thesis: ( A <> {} & f .: A = g .: B implies F $$ (A,f) = F $$ (B,g) )
assume ( A <> {} & f .: A = g .: B ) ; :: thesis: F $$ (A,f) = F $$ (B,g)
hence F $$ (A,f) = F $$ (B,g) by A23; :: thesis: verum