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 )
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 )
defpred S1[ 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 );
A2:
S1[ {}. C']
proof
assume A3:
(
{}. 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 A4:
(
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 &
{} = {}. C )
by A4, WELLORD2:def 4;
then
(
B = {}. C &
F $$ ({}. C'),
g = the_unity_wrt F )
by A1, A3, CARD_1:46, SETWISEO:40;
hence
F $$ ({}. C'),
g = F $$ B,
f
by A1, A3, SETWISEO:40;
:: thesis: verum
end;
A5:
for B' being Element of Fin C'
for b being Element of C' st S1[B'] & not b in B' holds
S1[B' \/ {.b.}]
proof
let A' be
Element of
Fin C';
:: thesis: for b being Element of C' st S1[A'] & not b in A' holds
S1[A' \/ {.b.}]let a be
Element of
C';
:: thesis: ( S1[A'] & not a in A' implies S1[A' \/ {.a.}] )
assume that A6:
( (
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 A7:
not
a in A'
;
:: thesis: S1[A' \/ {.a.}]
set A =
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 )
given s being
Function such that A8:
(
dom s = A' \/ {.a.} &
rng s = B &
s is
one-to-one )
and A9:
g | (A' \/ {.a.}) = f * s
;
:: thesis: F $$ (A' \/ {.a.}),g = F $$ B,f
A10:
a in A' \/ {.a.}
by SETWISEO:6;
then A11:
s . a in B
by A8, FUNCT_1:def 5;
B c= C
by FINSUB_1:def 5;
then reconsider c =
s . a as
Element of
C by A11;
a in C'
;
then
a in dom g
by FUNCT_2:def 1;
then
a in (dom g) /\ (A' \/ {.a.})
by A10, XBOOLE_0:def 4;
then
(
a in dom (f * s) &
g . a = (f * s) . a )
by A9, FUNCT_1:71, RELAT_1:90;
then A12:
g . a = f . c
by FUNCT_1:22;
set B' =
B \ {.c.};
set s' =
s | A';
A13:
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 A14:
x in dom (s | A')
and A15:
y = (s | A') . x
by FUNCT_1:def 5;
A16:
x in (dom s) /\ A'
by A14, RELAT_1:90;
then A17:
(
x in dom s &
x in A' )
by XBOOLE_0:def 4;
(
x in dom s &
x <> a )
by A7, A16, XBOOLE_0:def 4;
then
(
(s | A') . x = s . x &
s . x <> c )
by A8, A10, A14, FUNCT_1:70, FUNCT_1:def 8;
then
(
y in B & not
y in {c} )
by A8, A15, A17, FUNCT_1:def 5, TARSKI:def 1;
hence
y in B \ {.c.}
by XBOOLE_0:def 5;
:: thesis: verum
end; assume
y in B \ {.c.}
;
:: thesis: y in rng (s | A')then A18:
(
y in B & not
y in {c} )
by XBOOLE_0:def 5;
then consider x being
set such that A19:
x in dom s
and A20:
y = s . x
by A8, FUNCT_1:def 5;
(
x <> a & (
x in A' or
x in {a} ) )
by A8, A18, A19, A20, TARSKI:def 1, XBOOLE_0:def 3;
then
x in (dom s) /\ A'
by A19, 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 A20, FUNCT_1:def 5;
:: thesis: verum end;
A' c= A' \/ {.a.}
by XBOOLE_1:7;
then A21:
(
s | A' is
one-to-one &
dom (s | A') = A' &
rng (s | A') = B \ {.c.} )
by A8, A13, FUNCT_1:84, RELAT_1:91, TARSKI:2;
then A25:
dom (g | A') = dom (f * (s | A'))
by TARSKI:2;
for
x being
set st
x in dom (g | A') holds
(g | A') . x = (f * (s | A')) . x
then A31:
g | A' = f * (s | A')
by A25, FUNCT_1:9;
(B \ {.c.}) \/ {c} = B \/ {c}
by XBOOLE_1:39;
then A32:
(
B = (B \ {.c.}) \/ {c} & not
c in B \ {.c.} )
by A11, ZFMISC_1:46, ZFMISC_1:64;
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' )assume
y in f .: (B \ {.c.})
;
:: thesis: y in g .: A'then consider x being
set such that
x in dom f
and A36:
x in B \ {.c.}
and A37:
y = f . x
by FUNCT_1:def 12;
set x' =
((s | A') " ) . x;
A38:
((s | A') " ) . x in A'
by A21, A36, FUNCT_1:54;
A' c= C'
by FINSUB_1:def 5;
then
((s | A') " ) . x in C'
by A38;
then A39:
((s | A') " ) . x in dom g
by FUNCT_2:def 1;
(s | A') . (((s | A') " ) . x) = x
by A21, A36, FUNCT_1:57;
then y =
(f * (s | A')) . (((s | A') " ) . x)
by A21, A37, A38, FUNCT_1:23
.=
g . (((s | A') " ) . x)
by A31, A38, FUNCT_1:72
;
hence
y in g .: A'
by A38, A39, FUNCT_1:def 12;
:: thesis: verum end;
then A40:
f .: (B \ {.c.}) = g .: A'
by TARSKI:2;
now per cases
( A' = {} or A' <> {} )
;
suppose A41:
A' = {}
;
:: thesis: F $$ (A' \/ {.a.}),g = F $$ B,f
B \ {.c.} c= C
by FINSUB_1:def 5;
then
(
B \ {.c.} c= dom f &
g .: A' = {} )
by A41, FUNCT_2:def 1, RELAT_1:149;
then A42:
B \ {.c.} = {}
by A40;
thus F $$ (A' \/ {.a.}),
g =
f . c
by A1, A12, A41, SETWISEO:26
.=
F $$ B,
f
by A1, A32, A42, SETWISEO:26
;
:: thesis: verum end; suppose A43:
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 A44:
B \ {.c.} <> {}
by A40, A43, RELAT_1:149;
thus F $$ (A' \/ {.a.}),
g =
F . (F $$ A',g),
(g . a)
by A1, A7, A43, Th4
.=
F . (F $$ (B \ {.c.}),f),
(f . c)
by A6, A12, A21, A31, A43
.=
F $$ B,
f
by A1, A32, A44, Th4
;
:: thesis: verum end;
hence
F $$ (A' \/ {.a.}),
g = F $$ B,
f
;
:: thesis: verum
end;
for A being Element of Fin C' holds S1[A]
from SETWISEO:sch 2(A2, A5);
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