let C, C', D be non empty set ; :: thesis: for B being Element of Fin C
for A being Element of Fin C'
for F being BinOp of D
for f being Function of C,D
for g being Function of C',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 C'
for F being BinOp of D
for f being Function of C,D
for g being Function of C',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 C'; :: thesis: for F being BinOp of D
for f being Function of C,D
for g being Function of C',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 C',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 C',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 C',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 C'] 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 B' being Element of Fin C'
for b being Element of C' st S₁[B'] & not b in B' holds
S₁[B' \/ {.b.}]

proof

let A' be Element of Fin C'; :: thesis: for b being Element of C' st S₁[A'] & not b in A' holds
S₁[A' \/ {.b.}]
let a be Element of C'; :: thesis: ( S₁[A'] & not a in A' implies S₁[A' \/ {.a.}] )
assume that
A3: ( ( A' <> {} or F is having_a_unity ) implies for B being Element of Fin C st 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 ) and
A4: not a in A' ; :: thesis: S₁[A' \/ {.a.}]
assume ( A' \/ {a} <> {} or F is having_a_unity ) ; :: thesis: for B being Element of Fin C st ex s being Function st
( dom s = A' \/ {.a.} & rng s = B & s is one-to-one & g | (A' \/ {.a.}) = f * s ) holds
F $$ (A' \/ {.a.}),g = F $$ B,f
let B be Element of Fin C; :: thesis: ( ex s being Function st
( dom s = A' \/ {.a.} & rng s = B & s is one-to-one & g | (A' \/ {.a.}) = f * s ) implies F $$ (A' \/ {.a.}),g = F $$ B,f )
set A = A' \/ {.a.};
given s being Function such that A5: dom s = A' \/ {.a.} and
A6: rng s = B and
A7: s is one-to-one and
A8: g | (A' \/ {.a.}) = f * s ; :: thesis: F $$ (A' \/ {.a.}),g = F $$ B,f
A9: a in A' \/ {.a.} by SETWISEO:6;
then A10: s . a in B by A5, A6, FUNCT_1:def 5;
B c= C by FINSUB_1:def 5;
then reconsider c = s . a as Element of C by A10;
set B' = B \ {.c.};
set s' = s | A';
A11: s | A' is one-to-one by A7, FUNCT_1:84;

now

let y be set ; :: thesis: ( ( y in rng (s | A') implies y in B \ {.c.} ) & ( y in B \ {.c.} implies y in rng (s | A') ) )
thus ( y in rng (s | A') implies y in B \ {.c.} ) :: thesis: ( y in B \ {.c.} implies y in rng (s | A') )

proof

assume y in rng (s | A') ; :: thesis: y in B \ {.c.}
then consider x being set such that
A12: x in dom (s | A') and
A13: y = (s | A') . x by FUNCT_1:def 5;
A14: (s | A') . x = s . x by A12, FUNCT_1:70;
A15: x in (dom s) /\ A' by A12, RELAT_1:90;
then ( x in dom s & x <> a ) by A4, XBOOLE_0:def 4;
then s . x <> c by A5, A7, A9, FUNCT_1:def 8;
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 5;
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 | A')
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 5;
A20: ( x in A' 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) /\ A' by A18, A20, TARSKI:def 1, XBOOLE_0:def 4;
then ( x in dom (s | A') & (s | A') . x = s . x ) by FUNCT_1:71, RELAT_1:90;
hence y in rng (s | A') by A19, FUNCT_1:def 5; :: thesis: verum

end;

then A21: rng (s | A') = B \ {.c.} by TARSKI:2;

now

let x be set ; :: thesis: ( ( x in dom (g | A') implies x in dom (f * (s | A')) ) & ( x in dom (f * (s | A')) implies x in dom (g | A') ) )
thus ( x in dom (g | A') implies x in dom (f * (s | A')) ) :: thesis: ( x in dom (f * (s | A')) implies x in dom (g | A') )

proof

assume x in dom (g | A') ; :: thesis: x in dom (f * (s | A'))
then A22: x in (dom g) /\ A' by RELAT_1:90;
then A23: x in A' by XBOOLE_0:def 4;
A24: x in dom g by A22, XBOOLE_0:def 4;
x in A' \/ {.a.} by A23, SETWISEO:6;
then x in (dom g) /\ (A' \/ {.a.}) by A24, XBOOLE_0:def 4;
then A25: x in dom (f * s) by A8, RELAT_1:90;
then A26: s . x in dom f by FUNCT_1:21;
x in dom s by A25, FUNCT_1:21;
then x in (dom s) /\ A' by A23, XBOOLE_0:def 4;
then A27: x in dom (s | A') by RELAT_1:90;
then (s | A') . x = s . x by FUNCT_1:70;
hence x in dom (f * (s | A')) by A26, A27, FUNCT_1:21; :: thesis: verum

end;

assume A28: x in dom (f * (s | A')) ; :: thesis: x in dom (g | A')
then A29: x in dom (s | A') by FUNCT_1:21;
then A30: x in (dom s) /\ A' by RELAT_1:90;
then A31: x in dom s by XBOOLE_0:def 4;
(s | A') . x in dom f by A28, FUNCT_1:21;
then s . x in dom f by A29, FUNCT_1:70;
then x in dom (g | (A' \/ {.a.})) by A8, A31, FUNCT_1:21;
then x in (dom g) /\ (A' \/ {.a.}) by RELAT_1:90;
then A32: x in dom g by XBOOLE_0:def 4;
x in A' by A30, XBOOLE_0:def 4;
then x in (dom g) /\ A' by A32, XBOOLE_0:def 4;
hence x in dom (g | A') by RELAT_1:90; :: thesis: verum

end;

then A33: dom (g | A') = dom (f * (s | A')) by TARSKI:2;
a in C' ;
then a in dom g by FUNCT_2:def 1;
then a in (dom g) /\ (A' \/ {.a.}) by A9, XBOOLE_0:def 4;
then ( a in dom (f * s) & g . a = (f * s) . a ) by A8, FUNCT_1:71, RELAT_1:90;
then A34: g . a = f . c by FUNCT_1:22;
(B \ {.c.}) \/ {c} = B \/ {c} by XBOOLE_1:39;
then A35: B = (B \ {.c.}) \/ {c} by A10, ZFMISC_1:46;
A36: dom (s | A') = A' by A5, RELAT_1:91, XBOOLE_1:7;
A37: for x being set st x in dom (g | A') holds
(g | A') . x = (f * (s | A')) . x

proof

let x be set ; :: thesis: ( x in dom (g | A') implies (g | A') . x = (f * (s | A')) . x )
assume x in dom (g | A') ; :: thesis: (g | A') . x = (f * (s | A')) . x
then A38: x in (dom g) /\ A' by RELAT_1:90;
then A39: x in A' by XBOOLE_0:def 4;
then A40: x in A' \/ {.a.} by SETWISEO:6;
x in dom g by A38, XBOOLE_0:def 4;
then x in (dom g) /\ (A' \/ {.a.}) by A40, XBOOLE_0:def 4;
then x in dom (f * s) by A8, RELAT_1:90;
then A41: x in dom s by FUNCT_1:21;
then x in (dom s) /\ A' by A39, XBOOLE_0:def 4;
then A42: x in dom (s | A') by RELAT_1:90;
then A43: (s | A') . x = s . x by FUNCT_1:70;
thus (g | A') . x = g . x by A39, FUNCT_1:72
.= (f * s) . x by A8, A40, FUNCT_1:72
.= f . (s . x) by A41, FUNCT_1:23
.= (f * (s | A')) . x by A42, A43, FUNCT_1:23 ; :: thesis: verum

end;

then A44: g | A' = f * (s | A') by A33, FUNCT_1:9;

now

let y be set ; :: thesis: ( ( y in g .: A' implies y in f .: (B \ {.c.}) ) & ( y in f .: (B \ {.c.}) implies y in g .: A' ) )
thus ( y in g .: A' implies y in f .: (B \ {.c.}) ) :: thesis: ( y in f .: (B \ {.c.}) implies y in g .: A' )

proof

assume y in g .: A' ; :: thesis: y in f .: (B \ {.c.})
then consider x being set such that
A45: x in dom g and
A46: x in A' and
A47: y = g . x by FUNCT_1:def 12;
x in (dom g) /\ A' by A45, A46, XBOOLE_0:def 4;
then A48: x in dom (g | A') by RELAT_1:90;
then x in dom (s | A') by A33, FUNCT_1:21;
then A49: (s | A') . x in B \ {.c.} by A21, FUNCT_1:def 5;
y = (f * (s | A')) . x by A44, A46, A47, FUNCT_1:72;
then A50: y = f . ((s | A') . x) by A33, A48, FUNCT_1:22;
(s | A') . x in dom f by A33, A48, FUNCT_1:21;
hence y in f .: (B \ {.c.}) by A50, A49, FUNCT_1:def 12; :: thesis: verum

end;

assume y in f .: (B \ {.c.}) ; :: thesis: y in g .: A'
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 12;
set x' = ((s | A') " ) . x;
A53: ((s | A') " ) . x in A' by A11, A36, A21, A51, FUNCT_1:54;
A' c= C' by FINSUB_1:def 5;
then ((s | A') " ) . x in C' by A53;
then A54: ((s | A') " ) . x in dom g by FUNCT_2:def 1;
(s | A') . (((s | A') " ) . x) = x by A11, A21, A51, FUNCT_1:57;
then y = (f * (s | A')) . (((s | A') " ) . x) by A36, A52, A53, FUNCT_1:23
.= g . (((s | A') " ) . x) by A44, A53, FUNCT_1:72 ;
hence y in g .: A' by A53, A54, FUNCT_1:def 12; :: thesis: verum

end;

then A55: f .: (B \ {.c.}) = g .: A' by TARSKI:2;
A56: not c in B \ {.c.} by ZFMISC_1:64;

now

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

suppose A57: A' = {} ; :: thesis: F $$ (A' \/ {.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:149;
thus F $$ (A' \/ {.a.}),g = f . c by A1, A34, A57, SETWISEO:26
.= F $$ B,f by A1, A35, A58, SETWISEO:26 ; :: thesis: verum

end;

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

A' c= C' by FINSUB_1:def 5;
then A' c= dom g by FUNCT_2:def 1;
then A60: B \ {.c.} <> {} by A55, A59, RELAT_1:149;
thus F $$ (A' \/ {.a.}),g = F . (F $$ A',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:9
.= F $$ B,f by A1, A35, A56, A60, Th4 ; :: thesis: verum

end;

end;

end;

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

end;

A61: S₁[ {}. C']

proof

assume A62: ( {}. C' <> {} or F is having_a_unity ) ; :: thesis: for B being Element of Fin C st ex s being Function st
( dom s = {}. C' & rng s = B & s is one-to-one & g | ({}. C') = f * s ) holds
F $$ ({}. C'),g = F $$ B,f
let B be Element of Fin C; :: thesis: ( ex s being Function st
( dom s = {}. C' & rng s = B & s is one-to-one & g | ({}. C') = f * s ) implies F $$ ({}. C'),g = F $$ B,f )
given s being Function such that A63: ( dom s = {}. C' & rng s = B & s is one-to-one ) and
g | ({}. C') = f * s ; :: thesis: F $$ ({}. C'),g = F $$ B,f
B, {} are_equipotent by A63, WELLORD2:def 4;
then A64: B = {}. C by CARD_1:46;
F $$ ({}. C'),g = the_unity_wrt F by A1, A62, SETWISEO:40;
hence F $$ ({}. C'),g = F $$ B,f by A1, A62, A64, SETWISEO:40; :: thesis: verum

end;

for A being Element of Fin C' 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