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 A1: ( F is commutative & F is associative & 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
let A, B be Element of Fin X; :: thesis: ( A <> {} & f .: A = g .: B implies F $$ A,f = F $$ B,g )
assume that
A2: A <> {} and
A3: f .: A = g .: B ; :: thesis: 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: S₁[ {}. X] ;
A5: for B' being Element of Fin X
for b being Element of X st S₁[B'] holds
S₁[B' \/ {.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 A6: ( 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 A7: 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 x' being Element of X such that
A8: x' in A and
A9: f . x' = f . x by FUNCT_2:116;
A10: g .: B = (f .: A) \/ (Im f,x) by A7, RELAT_1:153
.= (f .: A) \/ {(f . x)} by Th13
.= f .: A by A8, A9, FUNCT_2:43, ZFMISC_1:46 ;
thus F $$ (A \/ {.x.}),f = F . (F $$ A,f),(f . x) by A1, A8, Th29
.= F . (F $$ (A \/ {.x'.}),f),(f . x) by A8, ZFMISC_1:46
.= F . (F . (F $$ A,f),(f . x')),(f . x) by A1, A8, Th29
.= F . (F $$ A,f),(F . (f . x'),(f . x')) by A1, A9, BINOP_1:def 3
.= F . (F $$ A,f),(f . x') by A1, BINOP_1:def 4
.= F $$ (A \/ {.x'.}),f by A1, A8, Th29
.= F $$ A,f by A8, ZFMISC_1:46
.= F $$ B,g by A6, A8, A10 ; :: thesis: verum

end;

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

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

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

then A13: g .: B = Im f,x by A7
.= {(f . x)} by Th13 ;
thus F $$ (A \/ {.x.}),f = f . x by A1, A12, Th26
.= F $$ B,g by A1, A13, Th34 ; :: thesis: verum

end;

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

reconsider B2 = B /\ (g " {(f . x)}) as Element of Fin X by Th16, XBOOLE_1:17;
reconsider B1 = B \ (g " {(f . x)}) as Element of Fin X by Th16;
A15: B = B1 \/ B2 by XBOOLE_1:51;

A16: now

assume B1 = {} ; :: thesis: contradiction
then B c= g " {(f . x)} by XBOOLE_1:37;
then A17: g .: B c= g .: (g " {(f . x)}) by RELAT_1:156;
A18: f .: A misses {(f . x)} by A11, ZFMISC_1:56;
g .: (g " {(f . x)}) c= {(f . x)} by FUNCT_1:145;
then f .: (A \/ {x}) c= {(f . x)} by A7, A17, 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 A18, XBOOLE_0:def 7 ;
hence contradiction by A14, Th19; :: thesis: verum

end;

x in A \/ {x} by Th6;
then f . x in g .: B by A7, FUNCT_2:43;
then consider x' being Element of X such that
A19: x' in B and
A20: g . x' = f . x by FUNCT_2:116;
x' in g " {(f . x)} by A20, Th12;
then A21: B2 <> {} by A19, XBOOLE_0:def 4;
A22: f .: A = (f .: A) \ {(f . x)} by A11, 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 A7, Th13
.= g .: B1 by Th11 ;
A23: 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;

thus F $$ (A \/ {.x.}),f = F . (F $$ A,f),(f . x) by A1, A14, Th29
.= F . (F $$ B1,g),(f . x) by A6, A14, A22
.= F . (F $$ B1,g),(F $$ B2,g) by A1, A21, A23, Th33
.= F $$ B,g by A1, A15, A16, A21, Th30 ; :: thesis: verum

end;

end;

end;

end;

end;

for A being Element of Fin X holds S₁[A] from SETWISEO:sch 4(A4, A5);
hence F $$ A,f = F $$ B,g by A2, A3; :: thesis: verum