let y be set ; for i, n being Nat st y c= Seg (n + 1) & i in Seg (n + 1) & not i in y holds
ex x being set st
( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n )
let i, n be Nat; ( y c= Seg (n + 1) & i in Seg (n + 1) & not i in y implies ex x being set st
( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n ) )
set x1 = { k where k is Element of NAT : ( k in y & k < i ) } ;
set x2 = { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ;
set x = { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ;
set f1 = id { k where k is Element of NAT : ( k in y & k < i ) } ;
assume A1:
y c= Seg (n + 1)
; ( not i in Seg (n + 1) or i in y or ex x being set st
( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n ) )
then A2:
y = rng (Sgm y)
by FINSEQ_1:def 13;
assume A3:
i in Seg (n + 1)
; ( i in y or ex x being set st
( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n ) )
then A4:
1 <= i
by FINSEQ_1:1;
A5:
i <= n + 1
by A3, FINSEQ_1:1;
then A14:
{ k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } c= Seg n
;
then reconsider x9 = { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } , y9 = y as finite set by A1;
set f2 = { [(k - 1),k] where k is Element of NAT : ( k in y9 & k > i ) } ;
now for x being object st x in { [(k - 1),k] where k is Element of NAT : ( k in y9 & k > i ) } holds
ex y, z being object st x = [y,z]let x be
object ;
( x in { [(k - 1),k] where k is Element of NAT : ( k in y9 & k > i ) } implies ex y, z being object st x = [y,z] )assume
x in { [(k - 1),k] where k is Element of NAT : ( k in y9 & k > i ) }
;
ex y, z being object st x = [y,z]then consider k being
Element of
NAT such that A15:
[(k - 1),k] = x
and
k in y9
and
k > i
;
reconsider y =
k - 1,
z =
k as
object ;
take y =
y;
ex z being object st x = [y,z]take z =
z;
x = [y,z]thus
x = [y,z]
by A15;
verum end;
then reconsider f2 = { [(k - 1),k] where k is Element of NAT : ( k in y9 & k > i ) } as Relation by RELAT_1:def 1;
set f = (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2;
then A21:
dom f2 = { (k - 1) where k is Element of NAT : ( k in y & k > i ) }
by A16, TARSKI:2;
A40:
now for x, y1, y2 being object st [x,y1] in f2 & [x,y2] in f2 holds
y1 = y2let x,
y1,
y2 be
object ;
( [x,y1] in f2 & [x,y2] in f2 implies y1 = y2 )assume
[x,y1] in f2
;
( [x,y2] in f2 implies y1 = y2 )then consider k being
Element of
NAT such that A41:
[(k - 1),k] = [x,y1]
and
k in y9
and
k > i
;
A42:
k - 1
= x
by A41, XTUPLE_0:1;
assume
[x,y2] in f2
;
y1 = y2then consider k9 being
Element of
NAT such that A43:
[(k9 - 1),k9] = [x,y2]
and
k9 in y9
and
k9 > i
;
k9 - 1
= x
by A43, XTUPLE_0:1;
hence
y1 = y2
by A41, A43, A42, XTUPLE_0:1;
verum end;
reconsider f = (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 as Function by A22, FUNCT_1:def 1;
reconsider f2 = f2 as Function by A40, FUNCT_1:def 1;
assume A48:
not i in y
; ex x being set st
( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n )
then A54:
rng f = y9
by A49, TARSKI:2;
now for a, b being object holds
( ( [a,b] in f implies [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) ) & ( [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) implies [a,b] in f ) )let a,
b be
object ;
( ( [a,b] in f implies [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) ) & ( [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) implies [b1,b2] in f ) )hereby ( [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) implies [b1,b2] in f )
assume A55:
[a,b] in f
;
[a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i}))per cases
( [a,b] in id { k where k is Element of NAT : ( k in y & k < i ) } or [a,b] in f2 )
by A55, XBOOLE_0:def 3;
suppose A56:
[a,b] in id { k where k is Element of NAT : ( k in y & k < i ) }
;
[a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i}))reconsider i9 =
i,
n9 =
n as
Element of
NAT by ORDINAL1:def 12;
A57:
a = b
by A56, RELAT_1:def 10;
a in { k where k is Element of NAT : ( k in y & k < i ) }
by A56, RELAT_1:def 10;
then consider a9 being
Element of
NAT such that A58:
a9 = a
and A59:
a9 in y
and A60:
a9 < i
;
A61:
1
<= a9
by A1, A59, FINSEQ_1:1;
i <= n + 1
by A3, FINSEQ_1:1;
then
a9 < n + 1
by A60, XXREAL_0:2;
then
a9 <= n
by NAT_1:13;
then A62:
a in Seg n
by A58, A61;
then
a in Seg (len (Sgm ((Seg (n + 1)) \ {i})))
by A3, FINSEQ_3:107;
then A63:
a in dom (Sgm ((Seg (n + 1)) \ {i}))
by FINSEQ_1:def 3;
a9 = (Sgm ((Seg (n9 + 1)) \ {i9})) . a9
by A3, A58, A60, A61, A62, FINSEQ_3:108;
then
[a,b] in Sgm ((Seg (n + 1)) \ {i})
by A57, A58, A63, FUNCT_1:1;
hence
[a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i}))
by A54, A57, A58, A59, RELAT_1:def 12;
verum end; suppose A64:
[a,b] in f2
;
[a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i}))reconsider i9 =
i,
n9 =
n as
Element of
NAT by ORDINAL1:def 12;
consider b9 being
Element of
NAT such that A65:
[a,b] = [(b9 - 1),b9]
and A66:
b9 in y9
and A67:
b9 > i
by A64;
A68:
a = b9 - 1
by A65, XTUPLE_0:1;
reconsider a9 =
b9 - 1 as
Integer ;
i + 1
<= b9
by A67, NAT_1:13;
then A69:
(i + 1) - 1
<= b9 - 1
by XREAL_1:9;
then A70:
1
<= a9
by A4, XXREAL_0:2;
reconsider a9 =
a9 as
Element of
NAT by A69, INT_1:3;
b9 <= n + 1
by A1, A66, FINSEQ_1:1;
then A71:
b9 - 1
<= (n + 1) - 1
by XREAL_1:9;
then A72:
a9 in Seg n
by A70;
then
a in Seg n
by A65, XTUPLE_0:1;
then
a in Seg (len (Sgm ((Seg (n + 1)) \ {i})))
by A3, FINSEQ_3:107;
then A73:
a in dom (Sgm ((Seg (n + 1)) \ {i}))
by FINSEQ_1:def 3;
a9 + 1
= (Sgm ((Seg (n9 + 1)) \ {i9})) . a9
by A3, A71, A69, A72, FINSEQ_3:108;
then
[a,b] in Sgm ((Seg (n + 1)) \ {i})
by A65, A68, A73, FUNCT_1:1;
hence
[a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i}))
by A54, A65, A66, RELAT_1:def 12;
verum end; end;
end; assume A74:
[a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i}))
;
[b1,b2] in fthen A75:
[a,b] in Sgm ((Seg (n + 1)) \ {i})
by RELAT_1:def 12;
then A76:
a in dom (Sgm ((Seg (n + 1)) \ {i}))
by XTUPLE_0:def 12;
b in rng f
by A74, RELAT_1:def 12;
then
b in Seg (n + 1)
by A1, A54;
then reconsider a9 =
a,
b9 =
b as
Element of
NAT by A76;
A77:
a in Seg (len (Sgm ((Seg (n + 1)) \ {i})))
by A76, FINSEQ_1:def 3;
then A78:
1
<= a9
by FINSEQ_1:1;
A79:
b in y
by A54, A74, RELAT_1:def 12;
A80:
a in Seg n
by A3, A77, FINSEQ_3:107;
reconsider i =
i,
n =
n as
Element of
NAT by ORDINAL1:def 12;
A81:
a9 <= n
by A80, FINSEQ_1:1;
per cases
( a9 < i or i <= a9 )
;
suppose A84:
i <= a9
;
[b1,b2] in fthen
(Sgm ((Seg (n + 1)) \ {i})) . a9 = a9 + 1
by A3, A80, A81, FINSEQ_3:108;
then A85:
b9 = a9 + 1
by A75, FUNCT_1:1;
then A86:
b9 > i
by A84, NAT_1:13;
A87:
a = b9 - 1
by A85;
b9 in y9
by A54, A74, RELAT_1:def 12;
then
[a,b] in f2
by A86, A87;
hence
[a,b] in f
by XBOOLE_0:def 3;
verum end; end; end;
then A88:
f = (rng f) |` (Sgm ((Seg (n + 1)) \ {i}))
;
reconsider g = f " as PartFunc of (dom (f ")),(rng (f ")) by RELSET_1:4;
then A109:
f is one-to-one
by FUNCT_1:def 4;
then
f " = f ~
by FUNCT_1:def 5;
then A110:
f " = ((Sgm ((Seg (n + 1)) \ {i})) ~) | (dom (f "))
by A88, Lm35;
dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) = { k where k is Element of NAT : ( k in y & k < i ) }
;
then A111:
dom f = x9
by A21, XTUPLE_0:23;
then
dom f c= NAT
by A14, XBOOLE_1:1;
then
rng g c= NAT
by A109, FUNCT_1:33;
then A112:
rng g c= REAL
by NUMBERS:19;
rng f c= NAT
by A1, A54, XBOOLE_1:1;
then
dom g c= NAT
by A109, FUNCT_1:33;
then
dom g c= REAL
by NUMBERS:19;
then reconsider g = g as PartFunc of REAL,REAL by A112, RELSET_1:7;
A113:
dom (f ") = y
by A109, A54, FUNCT_1:33;
then A128:
g | y is increasing
by RFUNCT_2:20;
A129:
rng (f ") = { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) }
by A109, A111, FUNCT_1:33;
then A130:
{ k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } = (f ") .: y
by A113, RELAT_1:113;
then A133:
g .: y c= NAT \ {0}
;
take
{ k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) }
; ( Sgm ( { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ) = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } c= Seg n )
Sgm ((Seg (n + 1)) \ {i}) is one-to-one
by FINSEQ_3:92, XBOOLE_1:36;
then A134:
(Sgm ((Seg (n + 1)) \ {i})) " = (Sgm ((Seg (n + 1)) \ {i})) ~
by FUNCT_1:def 5;
Sgm ( { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ) =
Sgm (g .: y)
by A113, A129, RELAT_1:113
.=
(((Sgm ((Seg (n + 1)) \ {i})) ") | y) * (Sgm y)
by A1, A113, A128, A133, A134, A110, Lm37
.=
((Sgm ((Seg (n + 1)) \ {i})) ") * (y |` (Sgm y))
by Lm36
.=
((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y)
by A2
;
hence
Sgm ( { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ) = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y)
; { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } c= Seg n
thus
{ k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } c= Seg n
by A6; verum