let y be set ; :: thesis: 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; :: thesis: ( 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) ; :: thesis: ( 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 y is included_in_Seg ;
then A2: y = rng (Sgm y) by FINSEQ_1:def 14;
assume A3: i in Seg (n + 1) ; :: thesis: ( 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;
A6: now :: thesis: for z being object st z in { 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 ) } holds
z in Seg n
let z be object ; :: thesis: ( z in { 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 ) } implies b1 in Seg n )
assume A7: z in { 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 ) } ; :: thesis: b1 in Seg n
per cases ( z in { k where k is Element of NAT : ( k in y & k < i ) } or z in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ) by A7, XBOOLE_0:def 3;
suppose z in { k where k is Element of NAT : ( k in y & k < i ) } ; :: thesis: b1 in Seg n
then A8: ex k being Element of NAT st
( k = z & k in y & k < i ) ;
then reconsider z9 = z as Element of NAT ;
z9 < n + 1 by A5, A8, XXREAL_0:2;
then A9: z9 <= n by NAT_1:13;
1 <= z9 by A1, A8, FINSEQ_1:1;
hence z in Seg n by A9; :: thesis: verum
end;
suppose z in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ; :: thesis: b1 in Seg n
then consider k being Element of NAT such that
A10: k - 1 = z and
A11: k in y and
A12: k > i ;
reconsider z9 = z as Integer by A10;
1 < k by A4, A12, XXREAL_0:2;
then 1 + 1 < k + 1 by XREAL_1:6;
then 2 <= k by NAT_1:13;
then A13: 2 - 1 <= k - 1 by XREAL_1:9;
then reconsider z9 = z9 as Element of NAT by A10, INT_1:3;
k <= n + 1 by A1, A11, FINSEQ_1:1;
then k - 1 <= (n + 1) - 1 by XREAL_1:9;
then z9 <= n by A10;
hence z in Seg n by A10, A13; :: thesis: verum
end;
end;
end;
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 :: thesis: 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 ; :: thesis: ( 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 ) } ; :: thesis: 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; :: thesis: ex z being object st x = [y,z]
take z = z; :: thesis: x = [y,z]
thus x = [y,z] by A15; :: thesis: 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;
A16: now :: thesis: for x being object st x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } holds
x in dom f2
let x be object ; :: thesis: ( x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } implies x in dom f2 )
assume x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ; :: thesis: x in dom f2
then consider k being Element of NAT such that
A17: ( k - 1 = x & k in y9 & k > i ) ;
reconsider y = k as set ;
[x,y] in f2 by A17;
hence x in dom f2 by XTUPLE_0:def 12; :: thesis: verum
end;
now :: thesis: for x being object st x in dom f2 holds
x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) }
let x be object ; :: thesis: ( x in dom f2 implies x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } )
assume x in dom f2 ; :: thesis: x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) }
then consider y being object such that
A18: [x,y] in f2 by XTUPLE_0:def 12;
consider k being Element of NAT such that
A19: [(k - 1),k] = [x,y] and
A20: ( k in y9 & k > i ) by A18;
k - 1 = x by A19, XTUPLE_0:1;
hence x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } by A20; :: thesis: verum
end;
then A21: dom f2 = { (k - 1) where k is Element of NAT : ( k in y & k > i ) } by A16, TARSKI:2;
A22: now :: thesis: for x, y1, y2 being object st [x,y1] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 & [x,y2] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 holds
y1 = y2
let x, y1, y2 be object ; :: thesis: ( [x,y1] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 & [x,y2] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 implies b2 = b3 )
assume A23: [x,y1] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 ; :: thesis: ( [x,y2] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 implies b2 = b3 )
assume A24: [x,y2] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 ; :: thesis: b2 = b3
A25: ( y1 is set & y2 is set ) by TARSKI:1;
per cases ( [x,y1] in id { k where k is Element of NAT : ( k in y & k < i ) } or [x,y1] in f2 ) by A23, XBOOLE_0:def 3;
suppose A26: [x,y1] in id { k where k is Element of NAT : ( k in y & k < i ) } ; :: thesis: b2 = b3
then A27: x in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) by XTUPLE_0:def 12;
then (id { k where k is Element of NAT : ( k in y & k < i ) } ) . x = x by FUNCT_1:17;
then A28: y1 = x by A26, A27, FUNCT_1:def 2, A25;
per cases ( [x,y2] in id { k where k is Element of NAT : ( k in y & k < i ) } or [x,y2] in f2 ) by A24, XBOOLE_0:def 3;
suppose A29: [x,y2] in id { k where k is Element of NAT : ( k in y & k < i ) } ; :: thesis: b2 = b3
then A30: x in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) by XTUPLE_0:def 12;
then (id { k where k is Element of NAT : ( k in y & k < i ) } ) . x = x by FUNCT_1:17;
hence y1 = y2 by A28, A29, A30, FUNCT_1:def 2, A25; :: thesis: verum
end;
suppose A31: [x,y2] in f2 ; :: thesis: b2 = b3
x in { k where k is Element of NAT : ( k in y & k < i ) } by A27;
then consider k9 being Element of NAT such that
A32: k9 = x and
k9 in y and
A33: k9 < i ;
x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } by A21, A31, XTUPLE_0:def 12;
then ex k being Element of NAT st
( k - 1 = x & k in y & k > i ) ;
then k9 + 1 > i by A32;
hence y1 = y2 by A33, NAT_1:13; :: thesis: verum
end;
end;
end;
suppose [x,y1] in f2 ; :: thesis: b2 = b3
then consider k being Element of NAT such that
A34: [(k - 1),k] = [x,y1] and
k in y9 and
A35: k > i ;
A36: k - 1 = x by A34, XTUPLE_0:1;
per cases ( [x,y2] in id { k where k is Element of NAT : ( k in y & k < i ) } or [x,y2] in f2 ) by A24, XBOOLE_0:def 3;
suppose [x,y2] in id { k where k is Element of NAT : ( k in y & k < i ) } ; :: thesis: b2 = b3
then x in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) by XTUPLE_0:def 12;
then x in { k where k is Element of NAT : ( k in y & k < i ) } ;
then consider k9 being Element of NAT such that
A37: k9 = x and
k9 in y and
A38: k9 < i ;
k9 = k - 1 by A34, A37, XTUPLE_0:1;
then k9 + 1 > i by A35;
hence y1 = y2 by A38, NAT_1:13; :: thesis: verum
end;
suppose [x,y2] in f2 ; :: thesis: b2 = b3
then consider k9 being Element of NAT such that
A39: [(k9 - 1),k9] = [x,y2] and
k9 in y9 and
k9 > i ;
k9 - 1 = x by A39, XTUPLE_0:1;
hence y1 = y2 by A34, A36, A39, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
end;
end;
A40: now :: thesis: for x, y1, y2 being object st [x,y1] in f2 & [x,y2] in f2 holds
y1 = y2
let x, y1, y2 be object ; :: thesis: ( [x,y1] in f2 & [x,y2] in f2 implies y1 = y2 )
assume [x,y1] in f2 ; :: thesis: ( [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 ; :: thesis: y1 = y2
then 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; :: thesis: 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;
A44: now :: thesis: for x being object st x in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) holds
f . x = (id { k where k is Element of NAT : ( k in y & k < i ) } ) . x
let x be object ; :: thesis: ( x in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) implies f . x = (id { k where k is Element of NAT : ( k in y & k < i ) } ) . x )
A45: id { k where k is Element of NAT : ( k in y & k < i ) } c= f by XBOOLE_1:7;
dom f = (dom (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (dom f2) by XTUPLE_0:23;
then A46: dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) c= dom f by XBOOLE_1:7;
assume A47: x in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) ; :: thesis: f . x = (id { k where k is Element of NAT : ( k in y & k < i ) } ) . x
then [x,((id { k where k is Element of NAT : ( k in y & k < i ) } ) . x)] in id { k where k is Element of NAT : ( k in y & k < i ) } by FUNCT_1:def 2;
hence f . x = (id { k where k is Element of NAT : ( k in y & k < i ) } ) . x by A47, A46, A45, FUNCT_1:def 2; :: thesis: verum
end;
reconsider f2 = f2 as Function by A40, FUNCT_1:def 1;
assume A48: not i in y ; :: thesis: ex x being set st
( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n )
A49: now :: thesis: for z being object st z in y9 holds
z in rng f
let z be object ; :: thesis: ( z in y9 implies b1 in rng f )
set k = z;
assume A50: z in y9 ; :: thesis: b1 in rng f
then z in Seg (n + 1) by A1;
then reconsider k = z as Element of NAT ;
per cases ( k <= i or k > i ) ;
suppose k <= i ; :: thesis: b1 in rng f
then k < i by A48, A50, XXREAL_0:1;
then z in { k where k is Element of NAT : ( k in y & k < i ) } by A50;
then z in rng (id { k where k is Element of NAT : ( k in y & k < i ) } ) ;
then z in (rng (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (rng f2) by XBOOLE_0:def 3;
hence z in rng f by RELAT_1:12; :: thesis: verum
end;
suppose A51: k > i ; :: thesis: b1 in rng f
set x99 = k - 1;
[(k - 1),z] in f2 by A50, A51;
then z in rng f2 by XTUPLE_0:def 13;
then z in (rng (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (rng f2) by XBOOLE_0:def 3;
hence z in rng f by RELAT_1:12; :: thesis: verum
end;
end;
end;
now :: thesis: for z being object st z in rng f holds
z in y9
let z be object ; :: thesis: ( z in rng f implies b1 in y9 )
assume z in rng f ; :: thesis: b1 in y9
then A52: z in (rng (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (rng f2) by RELAT_1:12;
per cases ( z in rng (id { k where k is Element of NAT : ( k in y & k < i ) } ) or z in rng f2 ) by A52, XBOOLE_0:def 3;
suppose z in rng (id { k where k is Element of NAT : ( k in y & k < i ) } ) ; :: thesis: b1 in y9
then z in { k where k is Element of NAT : ( k in y & k < i ) } ;
then ex k being Element of NAT st
( k = z & k in y & k < i ) ;
hence z in y9 ; :: thesis: verum
end;
suppose z in rng f2 ; :: thesis: b1 in y9
then consider x99 being object such that
A53: [x99,z] in f2 by XTUPLE_0:def 13;
ex k being Element of NAT st
( [(k - 1),k] = [x99,z] & k in y9 & k > i ) by A53;
hence z in y9 by XTUPLE_0:1; :: thesis: verum
end;
end;
end;
then A54: rng f = y9 by A49, TARSKI:2;
now :: thesis: 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 ; :: thesis: ( ( [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 :: thesis: ( [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) implies [b1,b2] in f )
assume A55: [a,b] in f ; :: thesis: [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 ) } ; :: thesis: [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; :: thesis: verum
end;
suppose A64: [a,b] in f2 ; :: thesis: [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; :: thesis: verum
end;
end;
end;
assume A74: [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) ; :: thesis: [b1,b2] in f
then 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 A82: a9 < i ; :: thesis: [b1,b2] in f
then (Sgm ((Seg (n + 1)) \ {i})) . a9 = a9 by A3, A80, A78, FINSEQ_3:108;
then A83: b = a by A75, FUNCT_1:1;
then a9 in { k where k is Element of NAT : ( k in y & k < i ) } by A79, A82;
then [a,b] in id { k where k is Element of NAT : ( k in y & k < i ) } by A83, RELAT_1:def 10;
hence [a,b] in f by XBOOLE_0:def 3; :: thesis: 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;
A89: now :: thesis: for x being set st x in dom f2 holds
f . x = f2 . x
let x be set ; :: thesis: ( x in dom f2 implies f . x = f2 . x )
A90: f2 c= f by XBOOLE_1:7;
dom f = (dom (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (dom f2) by XTUPLE_0:23;
then A91: dom f2 c= dom f by XBOOLE_1:7;
assume A92: x in dom f2 ; :: thesis: f . x = f2 . x
then [x,(f2 . x)] in f2 by FUNCT_1:def 2;
hence f . x = f2 . x by A92, A91, A90, FUNCT_1:def 2; :: thesis: verum
end;
now :: thesis: for y1, y2 being object st y1 in dom f & y2 in dom f & f . y1 = f . y2 holds
y1 = y2
let y1, y2 be object ; :: thesis: ( y1 in dom f & y2 in dom f & f . y1 = f . y2 implies b1 = b2 )
assume y1 in dom f ; :: thesis: ( y2 in dom f & f . y1 = f . y2 implies b1 = b2 )
then A93: y1 in (dom (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (dom f2) by XTUPLE_0:23;
assume y2 in dom f ; :: thesis: ( f . y1 = f . y2 implies b1 = b2 )
then A94: y2 in (dom (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (dom f2) by XTUPLE_0:23;
assume A95: f . y1 = f . y2 ; :: thesis: b1 = b2
per cases ( y1 in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) or y1 in dom f2 ) by A93, XBOOLE_0:def 3;
suppose A96: y1 in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) ; :: thesis: b1 = b2
then A97: (id { k where k is Element of NAT : ( k in y & k < i ) } ) . y1 = y1 by FUNCT_1:17;
then A98: f . y1 = y1 by A44, A96;
per cases ( y2 in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) or y2 in dom f2 ) by A94, XBOOLE_0:def 3;
suppose A99: y2 in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) ; :: thesis: b1 = b2
then (id { k where k is Element of NAT : ( k in y & k < i ) } ) . y2 = y2 by FUNCT_1:17;
hence y1 = y2 by A44, A95, A98, A99; :: thesis: verum
end;
suppose A100: y2 in dom f2 ; :: thesis: b1 = b2
then f . y2 = f2 . y2 by A89;
then [y2,(f . y2)] in f2 by A100, FUNCT_1:def 2;
then A101: ex k being Element of NAT st
( [(k - 1),k] = [y2,(f . y2)] & k in y9 & k > i ) ;
f . y1 = (id { k where k is Element of NAT : ( k in y & k < i ) } ) . y1 by A44, A96;
then f . y1 in { k where k is Element of NAT : ( k in y & k < i ) } by A96, A97;
then ex k9 being Element of NAT st
( k9 = f . y1 & k9 in y & k9 < i ) ;
hence y1 = y2 by A95, A101, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
suppose A102: y1 in dom f2 ; :: thesis: b1 = b2
then f . y1 = f2 . y1 by A89;
then [y1,(f . y1)] in f2 by A102, FUNCT_1:def 2;
then consider k being Element of NAT such that
A103: [(k - 1),k] = [y1,(f . y1)] and
k in y9 and
A104: k > i ;
A105: k = f . y1 by A103, XTUPLE_0:1;
per cases ( y2 in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) or y2 in dom f2 ) by A94, XBOOLE_0:def 3;
suppose A106: y2 in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) ; :: thesis: b1 = b2
then (id { k where k is Element of NAT : ( k in y & k < i ) } ) . y2 = y2 by FUNCT_1:17;
then f . y2 in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) by A44, A106;
then f . y2 in { k where k is Element of NAT : ( k in y & k < i ) } ;
then ex k9 being Element of NAT st
( k9 = f . y2 & k9 in y & k9 < i ) ;
hence y1 = y2 by A95, A103, A104, XTUPLE_0:1; :: thesis: verum
end;
suppose A107: y2 in dom f2 ; :: thesis: b1 = b2
then f . y2 = f2 . y2 by A89;
then [y2,(f . y2)] in f2 by A107, FUNCT_1:def 2;
then consider k being Element of NAT such that
A108: [(k - 1),k] = [y2,(f . y2)] and
k in y9 and
k > i ;
k = f . y2 by A108, XTUPLE_0:1;
hence y1 = y2 by A95, A103, A105, A108, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
end;
end;
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;
now :: thesis: for r1, r2 being Real st r1 in y /\ (dom g) & r2 in y /\ (dom g) & r1 < r2 holds
g . r1 < g . r2
let r1, r2 be Real; :: thesis: ( r1 in y /\ (dom g) & r2 in y /\ (dom g) & r1 < r2 implies g . b1 < g . b2 )
A114: g = ((id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2) ~ by A109, FUNCT_1:def 5
.= ((id { k where k is Element of NAT : ( k in y & k < i ) } ) ~) \/ (f2 ~) by RELAT_1:23 ;
assume r1 in y /\ (dom g) ; :: thesis: ( r2 in y /\ (dom g) & r1 < r2 implies g . b1 < g . b2 )
then A115: [r1,(g . r1)] in g by A113, FUNCT_1:1;
assume r2 in y /\ (dom g) ; :: thesis: ( r1 < r2 implies g . b1 < g . b2 )
then A116: [r2,(g . r2)] in g by A113, FUNCT_1:1;
assume A117: r1 < r2 ; :: thesis: g . b1 < g . b2
per cases ( [r1,(g . r1)] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) ~ or [r1,(g . r1)] in f2 ~ ) by A115, A114, XBOOLE_0:def 3;
suppose [r1,(g . r1)] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) ~ ; :: thesis: g . b1 < g . b2
then A118: [r1,(g . r1)] in id { k where k is Element of NAT : ( k in y & k < i ) } ;
then A119: r1 = g . r1 by RELAT_1:def 10;
r1 in { k where k is Element of NAT : ( k in y & k < i ) } by A118, RELAT_1:def 10;
then A120: ex k9 being Element of NAT st
( g . r1 = k9 & k9 in y & k9 < i ) by A119;
per cases ( [r2,(g . r2)] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) ~ or [r2,(g . r2)] in f2 ~ ) by A116, A114, XBOOLE_0:def 3;
suppose [r2,(g . r2)] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) ~ ; :: thesis: g . b1 < g . b2
then [r2,(g . r2)] in id { k where k is Element of NAT : ( k in y & k < i ) } ;
hence g . r1 < g . r2 by A117, A119, RELAT_1:def 10; :: thesis: verum
end;
suppose [r2,(g . r2)] in f2 ~ ; :: thesis: g . b1 < g . b2
then [(g . r2),r2] in f2 by RELAT_1:def 7;
then consider k99 being Element of NAT such that
A121: [(k99 - 1),k99] = [(g . r2),r2] and
k99 in y9 and
A122: k99 > i ;
reconsider k999 = g . r2, i9 = i - 1 as Integer by A121, XTUPLE_0:1;
k99 - 1 = g . r2 by A121, XTUPLE_0:1;
then i - 1 < g . r2 by A122, XREAL_1:9;
then i9 + 1 <= k999 by INT_1:7;
hence g . r1 < g . r2 by A120, XXREAL_0:2; :: thesis: verum
end;
end;
end;
suppose [r1,(g . r1)] in f2 ~ ; :: thesis: g . b1 < g . b2
then [(g . r1),r1] in f2 by RELAT_1:def 7;
then consider k9 being Element of NAT such that
A123: [(k9 - 1),k9] = [(g . r1),r1] and
k9 in y9 and
A124: k9 > i ;
A125: k9 - 1 = g . r1 by A123, XTUPLE_0:1;
A126: r1 = k9 by A123, XTUPLE_0:1;
per cases ( [r2,(g . r2)] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) ~ or [r2,(g . r2)] in f2 ~ ) by A116, A114, XBOOLE_0:def 3;
suppose [r2,(g . r2)] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) ~ ; :: thesis: g . b1 < g . b2
then [r2,(g . r2)] in id { k where k is Element of NAT : ( k in y & k < i ) } ;
then r2 in { k where k is Element of NAT : ( k in y & k < i ) } by RELAT_1:def 10;
then ex k99 being Element of NAT st
( r2 = k99 & k99 in y & k99 < i ) ;
hence g . r1 < g . r2 by A117, A124, A126, XXREAL_0:2; :: thesis: verum
end;
suppose [r2,(g . r2)] in f2 ~ ; :: thesis: g . b1 < g . b2
then [(g . r2),r2] in f2 by RELAT_1:def 7;
then consider k99 being Element of NAT such that
A127: [(k99 - 1),k99] = [(g . r2),r2] and
k99 in y9 and
k99 > i ;
( k99 - 1 = g . r2 & r2 = k99 ) by A127, XTUPLE_0:1;
hence g . r1 < g . r2 by A117, A125, A126, XREAL_1:9; :: thesis: verum
end;
end;
end;
end;
end;
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;
now :: thesis: for x9 being object st x9 in g .: y holds
x9 in NAT \ {0}
let x9 be object ; :: thesis: ( x9 in g .: y implies x9 in NAT \ {0} )
assume A131: x9 in g .: y ; :: thesis: x9 in NAT \ {0}
then not x9 = 0 by A14, A130, FINSEQ_1:1;
then A132: not x9 in {0} by TARSKI:def 1;
x9 in Seg n by A6, A130, A131;
hence x9 in NAT \ {0} by A132, XBOOLE_0:def 5; :: thesis: verum
end;
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 ) } ; :: thesis: ( 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;
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) ; :: thesis: { 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; :: thesis: verum