let C, C9, D be non empty set ; :: thesis: for B being Element of Fin C
for A being Element of Fin C9
for F being BinOp of D
for f being Function of C,D
for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st
( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds
F \$\$ (A,g) = F \$\$ (B,f)

let B be Element of Fin C; :: thesis: for A being Element of Fin C9
for F being BinOp of D
for f being Function of C,D
for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st
( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds
F \$\$ (A,g) = F \$\$ (B,f)

let A be Element of Fin C9; :: thesis: for F being BinOp of D
for f being Function of C,D
for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st
( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds
F \$\$ (A,g) = F \$\$ (B,f)

let F be BinOp of D; :: thesis: for f being Function of C,D
for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st
( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds
F \$\$ (A,g) = F \$\$ (B,f)

let f be Function of C,D; :: thesis: for g being Function of C9,D st F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st
( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) holds
F \$\$ (A,g) = F \$\$ (B,f)

let g be Function of C9,D; :: thesis: ( F is commutative & F is associative & ( A <> {} or F is having_a_unity ) & ex s being Function st
( dom s = A & rng s = B & s is one-to-one & g | A = f * s ) implies F \$\$ (A,g) = F \$\$ (B,f) )

defpred S1[ Element of Fin C9] means ( ( \$1 <> {} or F is having_a_unity ) implies for B being Element of Fin C st ex s being Function st
( dom s = \$1 & rng s = B & s is one-to-one & g | \$1 = f * s ) holds
F \$\$ (\$1,g) = F \$\$ (B,f) );
assume A1: ( F is commutative & F is associative ) ; :: thesis: ( ( not A <> {} & not F is having_a_unity ) or for s being Function holds
( not dom s = A or not rng s = B or not s is one-to-one or not g | A = f * s ) or F \$\$ (A,g) = F \$\$ (B,f) )

A2: for B9 being Element of Fin C9
for b being Element of C9 st S1[B9] & not b in B9 holds
S1[B9 \/ {.b.}]
proof
let A9 be Element of Fin C9; :: thesis: for b being Element of C9 st S1[A9] & not b in A9 holds
S1[A9 \/ {.b.}]

let a be Element of C9; :: thesis: ( S1[A9] & not a in A9 implies S1[A9 \/ {.a.}] )
assume that
A3: ( ( A9 <> {} or F is having_a_unity ) implies for B being Element of Fin C st ex s being Function st
( dom s = A9 & rng s = B & s is one-to-one & g | A9 = f * s ) holds
F \$\$ (A9,g) = F \$\$ (B,f) ) and
A4: not a in A9 ; :: thesis: S1[A9 \/ {.a.}]
assume ( A9 \/ {a} <> {} or F is having_a_unity ) ; :: thesis: for B being Element of Fin C st ex s being Function st
( dom s = A9 \/ {.a.} & rng s = B & s is one-to-one & g | (A9 \/ {.a.}) = f * s ) holds
F \$\$ ((A9 \/ {.a.}),g) = F \$\$ (B,f)

let B be Element of Fin C; :: thesis: ( ex s being Function st
( dom s = A9 \/ {.a.} & rng s = B & s is one-to-one & g | (A9 \/ {.a.}) = f * s ) implies F \$\$ ((A9 \/ {.a.}),g) = F \$\$ (B,f) )

set A = A9 \/ {.a.};
given s being Function such that A5: dom s = A9 \/ {.a.} and
A6: rng s = B and
A7: s is one-to-one and
A8: g | (A9 \/ {.a.}) = f * s ; :: thesis: F \$\$ ((A9 \/ {.a.}),g) = F \$\$ (B,f)
A9: a in A9 \/ {.a.} by ZFMISC_1:136;
then A10: s . a in B by ;
B c= C by FINSUB_1:def 5;
then reconsider c = s . a as Element of C by A10;
set B9 = B \ {.c.};
set s9 = s | A9;
A11: s | A9 is one-to-one by ;
now :: thesis: for y being object holds
( ( y in rng (s | A9) implies y in B \ {.c.} ) & ( y in B \ {.c.} implies y in rng (s | A9) ) )
let y be object ; :: thesis: ( ( y in rng (s | A9) implies y in B \ {.c.} ) & ( y in B \ {.c.} implies y in rng (s | A9) ) )
thus ( y in rng (s | A9) implies y in B \ {.c.} ) :: thesis: ( y in B \ {.c.} implies y in rng (s | A9) )
proof
assume y in rng (s | A9) ; :: thesis: y in B \ {.c.}
then consider x being object such that
A12: x in dom (s | A9) and
A13: y = (s | A9) . x by FUNCT_1:def 3;
A14: (s | A9) . x = s . x by ;
A15: x in (dom s) /\ A9 by ;
then ( x in dom s & x <> a ) by ;
then s . x <> c by ;
then A16: not y in {c} by ;
x in dom s by ;
then y in B by ;
hence y in B \ {.c.} by ; :: thesis: verum
end;
assume A17: y in B \ {.c.} ; :: thesis: y in rng (s | A9)
then y in B by XBOOLE_0:def 5;
then consider x being object such that
A18: x in dom s and
A19: y = s . x by ;
A20: ( x in A9 or x in {a} ) by ;
not y in {c} by ;
then x <> a by ;
then x in (dom s) /\ A9 by ;
then ( x in dom (s | A9) & (s | A9) . x = s . x ) by ;
hence y in rng (s | A9) by ; :: thesis: verum
end;
then A21: rng (s | A9) = B \ {.c.} by TARSKI:2;
now :: thesis: for x being object holds
( ( x in dom (g | A9) implies x in dom (f * (s | A9)) ) & ( x in dom (f * (s | A9)) implies x in dom (g | A9) ) )
let x be object ; :: thesis: ( ( x in dom (g | A9) implies x in dom (f * (s | A9)) ) & ( x in dom (f * (s | A9)) implies x in dom (g | A9) ) )
thus ( x in dom (g | A9) implies x in dom (f * (s | A9)) ) :: thesis: ( x in dom (f * (s | A9)) implies x in dom (g | A9) )
proof
assume x in dom (g | A9) ; :: thesis: x in dom (f * (s | A9))
then A22: x in (dom g) /\ A9 by RELAT_1:61;
then A23: x in A9 by XBOOLE_0:def 4;
A24: x in dom g by ;
x in A9 \/ {.a.} by ;
then x in (dom g) /\ (A9 \/ {.a.}) by ;
then A25: x in dom (f * s) by ;
then A26: s . x in dom f by FUNCT_1:11;
x in dom s by ;
then x in (dom s) /\ A9 by ;
then A27: x in dom (s | A9) by RELAT_1:61;
then (s | A9) . x = s . x by FUNCT_1:47;
hence x in dom (f * (s | A9)) by ; :: thesis: verum
end;
assume A28: x in dom (f * (s | A9)) ; :: thesis: x in dom (g | A9)
then A29: x in dom (s | A9) by FUNCT_1:11;
then A30: x in (dom s) /\ A9 by RELAT_1:61;
then A31: x in dom s by XBOOLE_0:def 4;
(s | A9) . x in dom f by ;
then s . x in dom f by ;
then x in dom (g | (A9 \/ {.a.})) by ;
then x in (dom g) /\ (A9 \/ {.a.}) by RELAT_1:61;
then A32: x in dom g by XBOOLE_0:def 4;
x in A9 by ;
then x in (dom g) /\ A9 by ;
hence x in dom (g | A9) by RELAT_1:61; :: thesis: verum
end;
then A33: dom (g | A9) = dom (f * (s | A9)) by TARSKI:2;
a in C9 ;
then a in dom g by FUNCT_2:def 1;
then a in (dom g) /\ (A9 \/ {.a.}) by ;
then ( a in dom (f * s) & g . a = (f * s) . a ) by ;
then A34: g . a = f . c by FUNCT_1:12;
(B \ {.c.}) \/ {c} = B \/ {c} by XBOOLE_1:39;
then A35: B = (B \ {.c.}) \/ {c} by ;
A36: dom (s | A9) = A9 by ;
A37: for x being object st x in dom (g | A9) holds
(g | A9) . x = (f * (s | A9)) . x
proof
let x be object ; :: thesis: ( x in dom (g | A9) implies (g | A9) . x = (f * (s | A9)) . x )
assume x in dom (g | A9) ; :: thesis: (g | A9) . x = (f * (s | A9)) . x
then A38: x in (dom g) /\ A9 by RELAT_1:61;
then A39: x in A9 by XBOOLE_0:def 4;
then A40: x in A9 \/ {.a.} by ZFMISC_1:136;
x in dom g by ;
then x in (dom g) /\ (A9 \/ {.a.}) by ;
then x in dom (f * s) by ;
then A41: x in dom s by FUNCT_1:11;
then x in (dom s) /\ A9 by ;
then A42: x in dom (s | A9) by RELAT_1:61;
then A43: (s | A9) . x = s . x by FUNCT_1:47;
thus (g | A9) . x = g . x by
.= (f * s) . x by
.= f . (s . x) by
.= (f * (s | A9)) . x by ; :: thesis: verum
end;
then A44: g | A9 = f * (s | A9) by ;
now :: thesis: for y being object holds
( ( y in g .: A9 implies y in f .: (B \ {.c.}) ) & ( y in f .: (B \ {.c.}) implies y in g .: A9 ) )
let y be object ; :: thesis: ( ( y in g .: A9 implies y in f .: (B \ {.c.}) ) & ( y in f .: (B \ {.c.}) implies y in g .: A9 ) )
thus ( y in g .: A9 implies y in f .: (B \ {.c.}) ) :: thesis: ( y in f .: (B \ {.c.}) implies y in g .: A9 )
proof
assume y in g .: A9 ; :: thesis: y in f .: (B \ {.c.})
then consider x being object such that
A45: x in dom g and
A46: x in A9 and
A47: y = g . x by FUNCT_1:def 6;
x in (dom g) /\ A9 by ;
then A48: x in dom (g | A9) by RELAT_1:61;
then x in dom (s | A9) by ;
then A49: (s | A9) . x in B \ {.c.} by ;
y = (f * (s | A9)) . x by ;
then A50: y = f . ((s | A9) . x) by ;
(s | A9) . x in dom f by ;
hence y in f .: (B \ {.c.}) by ; :: thesis: verum
end;
assume y in f .: (B \ {.c.}) ; :: thesis: y in g .: A9
then consider x being object such that
x in dom f and
A51: x in B \ {.c.} and
A52: y = f . x by FUNCT_1:def 6;
set x9 = ((s | A9) ") . x;
A53: ((s | A9) ") . x in A9 by ;
A9 c= C9 by FINSUB_1:def 5;
then ((s | A9) ") . x in C9 by A53;
then A54: ((s | A9) ") . x in dom g by FUNCT_2:def 1;
(s | A9) . (((s | A9) ") . x) = x by ;
then y = (f * (s | A9)) . (((s | A9) ") . x) by
.= g . (((s | A9) ") . x) by ;
hence y in g .: A9 by ; :: thesis: verum
end;
then A55: f .: (B \ {.c.}) = g .: A9 by TARSKI:2;
A56: not c in B \ {.c.} by ZFMISC_1:56;
now :: thesis: F \$\$ ((A9 \/ {.a.}),g) = F \$\$ (B,f)
per cases ( A9 = {} or A9 <> {} ) ;
suppose A57: A9 = {} ; :: thesis: F \$\$ ((A9 \/ {.a.}),g) = F \$\$ (B,f)
B \ {.c.} c= C by FINSUB_1:def 5;
then B \ {.c.} c= dom f by FUNCT_2:def 1;
then A58: B \ {.c.} = {} by ;
thus F \$\$ ((A9 \/ {.a.}),g) = f . c by
.= F \$\$ (B,f) by ; :: thesis: verum
end;
suppose A59: A9 <> {} ; :: thesis: F \$\$ ((A9 \/ {.a.}),g) = F \$\$ (B,f)
A9 c= C9 by FINSUB_1:def 5;
then A9 c= dom g by FUNCT_2:def 1;
then A60: B \ {.c.} <> {} by ;
thus F \$\$ ((A9 \/ {.a.}),g) = F . ((F \$\$ (A9,g)),(g . a)) by A1, A4, A59, Th2
.= F . ((F \$\$ ((B \ {.c.}),f)),(f . c)) by A3, A34, A11, A36, A21, A33, A37, A59, FUNCT_1:2
.= F \$\$ (B,f) by A1, A35, A56, A60, Th2 ; :: thesis: verum
end;
end;
end;
hence F \$\$ ((A9 \/ {.a.}),g) = F \$\$ (B,f) ; :: thesis: verum
end;
A61: S1[ {}. C9]
proof
assume A62: ( {}. C9 <> {} or F is having_a_unity ) ; :: thesis: for B being Element of Fin C st ex s being Function st
( dom s = {}. C9 & rng s = B & s is one-to-one & g | ({}. C9) = f * s ) holds
F \$\$ (({}. C9),g) = F \$\$ (B,f)

let B be Element of Fin C; :: thesis: ( ex s being Function st
( dom s = {}. C9 & rng s = B & s is one-to-one & g | ({}. C9) = f * s ) implies F \$\$ (({}. C9),g) = F \$\$ (B,f) )

given s being Function such that A63: ( dom s = {}. C9 & rng s = B & s is one-to-one ) and
g | ({}. C9) = f * s ; :: thesis: F \$\$ (({}. C9),g) = F \$\$ (B,f)
B, {} are_equipotent by ;
then A64: B = {}. C by CARD_1:26;
F \$\$ (({}. C9),g) = the_unity_wrt F by ;
hence F \$\$ (({}. C9),g) = F \$\$ (B,f) by ; :: thesis: verum
end;
for A being Element of Fin C9 holds S1[A] from hence ( ( not A <> {} & not F is having_a_unity ) or for s being Function holds
( not dom s = A or not rng s = B or not s is one-to-one or not g | A = f * s ) or F \$\$ (A,g) = F \$\$ (B,f) ) ; :: thesis: verum