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:116;
A9: g .: B = (f .: A) \/ (Im f,x) by A6, RELAT_1:153
.= (f .: A) \/ {(f . x)} by Th13
.= f .: A by A7, A8, FUNCT_2:43, ZFMISC_1:46 ;
thus F $$ (A \/ {.x.}),f = F . (F $$ A,f),(f . x) by A1, A2, A3, A7, Th29
.= F . (F $$ (A \/ {.x9.}),f),(f . x) by A7, ZFMISC_1:46
.= F . (F . (F $$ A,f),(f . x9)),(f . x) by A1, A2, A3, A7, Th29
.= F . (F $$ A,f),(F . (f . x9),(f . x9)) by A2, A8, BINOP_1:def 3
.= F . (F $$ A,f),(f . x9) by A3, BINOP_1:def 4
.= F $$ (A \/ {.x9.}),f by A1, A2, A3, A7, Th29
.= F $$ A,f by A7, ZFMISC_1:46
.= 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 Th13 ;
thus F $$ (A \/ {.x.}),f = f . x by A1, A2, A11, Th26
.= F $$ B,g by A1, A2, A3, A12, Th34 ; :: 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 Th16;

A14: now

assume B1 = {} ; :: thesis: contradiction
then B c= g " {(f . x)} by XBOOLE_1:37;
then A15: g .: B c= g .: (g " {(f . x)}) by RELAT_1:156;
A16: f .: A misses {(f . x)} by A10, ZFMISC_1:56;
g .: (g " {(f . x)}) c= {(f . x)} by FUNCT_1:145;
then f .: (A \/ {x}) c= {(f . x)} by A6, A15, XBOOLE_1:1;
then (f .: A) \/ (f .: {x}) c= {(f . x)} by RELAT_1:153;
then f .: A = (f .: A) /\ {(f . x)} by XBOOLE_1:11, XBOOLE_1:28
.= {} by A16, XBOOLE_0:def 7 ;
hence contradiction by A13, Th19; :: thesis: verum

end;

reconsider B2 = B /\ (g " {(f . x)}) as Element of Fin X by Th16, XBOOLE_1:17;
A17: B = B1 \/ B2 by XBOOLE_1:51;
A18: 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 13;
hence g . b = f . x by TARSKI:def 1; :: thesis: verum

end;

A19: f .: A = (f .: A) \ {(f . x)} by A10, ZFMISC_1:65
.= (f .: A) \ (Im f,x) by Th13
.= ((f .: A) \/ (f .: {x})) \ (f .: {x}) by XBOOLE_1:40
.= (f .: (A \/ {x})) \ (Im f,x) by RELAT_1:153
.= (g .: B) \ {(f . x)} by A6, Th13
.= g .: B1 by Th11 ;
x in A \/ {x} by Th6;
then consider x9 being Element of X such that
A20: x9 in B and
A21: g . x9 = f . x by A6, FUNCT_2:43, FUNCT_2:116;
x9 in g " {(f . x)} by A21, Th12;
then A22: B2 <> {} by A20, XBOOLE_0:def 4;
thus F $$ (A \/ {.x.}),f = F . (F $$ A,f),(f . x) by A1, A2, A3, A13, Th29
.= F . (F $$ B1,g),(f . x) by A5, A13, A19
.= F . (F $$ B1,g),(F $$ B2,g) by A1, A2, A3, A22, A18, Th33
.= F $$ B,g by A1, A2, A3, A17, A14, A22, Th30 ; :: thesis: verum

end;

end;

end;

end;

end;

A23: S₁[ {}. X] ;
A24: for A being Element of Fin X holds S₁[A] from SETWISEO:sch 4(A23, 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 A24; :: thesis: verum