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 S₁[ 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 S₁[B9] & not b in B9 holds
S₁[B9 \/ {.b.}]

proof

let A9 be Element of Fin C9; :: thesis: for b being Element of C9 st S₁[A9] & not b in A9 holds
S₁[A9 \/ {.b.}]
let a be Element of C9; :: thesis: ( S₁[A9] & not a in A9 implies S₁[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: S₁[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 SETWISEO:4;
then A10: s . a in B by A5, A6, FUNCT_1:def 3;
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 A7, FUNCT_1:52;

now

let y be set ; :: 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 set 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 A12, FUNCT_1:47;
A15: x in (dom s) /\ A9 by A12, RELAT_1:61;
then ( x in dom s & x <> a ) by A4, XBOOLE_0:def 4;
then s . x <> c by A5, A7, A9, FUNCT_1:def 4;
then A16: not y in {c} by A13, A14, TARSKI:def 1;
x in dom s by A15, XBOOLE_0:def 4;
then y in B by A6, A13, A14, FUNCT_1:def 3;
hence y in B \ {.c.} by A16, XBOOLE_0:def 5; :: 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 set such that
A18: x in dom s and
A19: y = s . x by A6, FUNCT_1:def 3;
A20: ( x in A9 or x in {a} ) by A5, A18, XBOOLE_0:def 3;
not y in {c} by A17, XBOOLE_0:def 5;
then x <> a by A19, TARSKI:def 1;
then x in (dom s) /\ A9 by A18, A20, TARSKI:def 1, XBOOLE_0:def 4;
then ( x in dom (s | A9) & (s | A9) . x = s . x ) by FUNCT_1:48, RELAT_1:61;
hence y in rng (s | A9) by A19, FUNCT_1:def 3; :: thesis: verum

end;

then A21: rng (s | A9) = B \ {.c.} by TARSKI:1;

now

let x be set ; :: 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 A22, XBOOLE_0:def 4;
x in A9 \/ {.a.} by A23, SETWISEO:4;
then x in (dom g) /\ (A9 \/ {.a.}) by A24, XBOOLE_0:def 4;
then A25: x in dom (f * s) by A8, RELAT_1:61;
then A26: s . x in dom f by FUNCT_1:11;
x in dom s by A25, FUNCT_1:11;
then x in (dom s) /\ A9 by A23, XBOOLE_0:def 4;
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 A26, A27, FUNCT_1:11; :: 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 A28, FUNCT_1:11;
then s . x in dom f by A29, FUNCT_1:47;
then x in dom (g | (A9 \/ {.a.})) by A8, A31, FUNCT_1:11;
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 A30, XBOOLE_0:def 4;
then x in (dom g) /\ A9 by A32, XBOOLE_0:def 4;
hence x in dom (g | A9) by RELAT_1:61; :: thesis: verum

end;

then A33: dom (g | A9) = dom (f * (s | A9)) by TARSKI:1;
a in C9 ;
then a in dom g by FUNCT_2:def 1;
then a in (dom g) /\ (A9 \/ {.a.}) by A9, XBOOLE_0:def 4;
then ( a in dom (f * s) & g . a = (f * s) . a ) by A8, FUNCT_1:48, RELAT_1:61;
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 A10, ZFMISC_1:40;
A36: dom (s | A9) = A9 by A5, RELAT_1:62, XBOOLE_1:7;
A37: for x being set st x in dom (g | A9) holds
(g | A9) . x = (f * (s | A9)) . x

proof

let x be set ; :: 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 SETWISEO:4;
x in dom g by A38, XBOOLE_0:def 4;
then x in (dom g) /\ (A9 \/ {.a.}) by A40, XBOOLE_0:def 4;
then x in dom (f * s) by A8, RELAT_1:61;
then A41: x in dom s by FUNCT_1:11;
then x in (dom s) /\ A9 by A39, XBOOLE_0:def 4;
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 A39, FUNCT_1:49
.= (f * s) . x by A8, A40, FUNCT_1:49
.= f . (s . x) by A41, FUNCT_1:13
.= (f * (s | A9)) . x by A42, A43, FUNCT_1:13 ; :: thesis: verum

end;

then A44: g | A9 = f * (s | A9) by A33, FUNCT_1:2;

now

let y be set ; :: 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 set 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 A45, A46, XBOOLE_0:def 4;
then A48: x in dom (g | A9) by RELAT_1:61;
then x in dom (s | A9) by A33, FUNCT_1:11;
then A49: (s | A9) . x in B \ {.c.} by A21, FUNCT_1:def 3;
y = (f * (s | A9)) . x by A44, A46, A47, FUNCT_1:49;
then A50: y = f . ((s | A9) . x) by A33, A48, FUNCT_1:12;
(s | A9) . x in dom f by A33, A48, FUNCT_1:11;
hence y in f .: (B \ {.c.}) by A50, A49, FUNCT_1:def 6; :: thesis: verum

end;

assume y in f .: (B \ {.c.}) ; :: thesis: y in g .: A9
then consider x being set 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 A11, A36, A21, A51, FUNCT_1:32;
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 A11, A21, A51, FUNCT_1:35;
then y = (f * (s | A9)) . (((s | A9) ") . x) by A36, A52, A53, FUNCT_1:13
.= g . (((s | A9) ") . x) by A44, A53, FUNCT_1:49 ;
hence y in g .: A9 by A53, A54, FUNCT_1:def 6; :: thesis: verum

end;

then A55: f .: (B \ {.c.}) = g .: A9 by TARSKI:1;
A56: not c in B \ {.c.} by ZFMISC_1:56;

now

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 A55, A57, RELAT_1:116;
thus F $$ ((A9 \/ {.a.}),g) = f . c by A1, A34, A57, SETWISEO:17
.= F $$ (B,f) by A1, A35, A58, SETWISEO:17 ; :: 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 A55, A59, RELAT_1:116;
thus F $$ ((A9 \/ {.a.}),g) = F . ((F $$ (A9,g)),(g . a)) by A1, A4, A59, Th4
.= 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, Th4 ; :: thesis: verum

end;

end;

end;

hence F $$ ((A9 \/ {.a.}),g) = F $$ (B,f) ; :: thesis: verum

end;

A61: S₁[ {}. 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 A63, WELLORD2:def 4;
then A64: B = {}. C by CARD_1:26;
F $$ (({}. C9),g) = the_unity_wrt F by A1, A62, SETWISEO:31;
hence F $$ (({}. C9),g) = F $$ (B,f) by A1, A62, A64, SETWISEO:31; :: thesis: verum

end;

for A being Element of Fin C9 holds S₁[A] from SETWISEO:sch 2(A61, A2);
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