let y be set ; :: thesis: for n, i 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 n, i 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 A2: y = rng (Sgm y) by FINSEQ_1:def 13;
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
let z be set ; :: 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 number 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 by TARSKI:def 3;
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
let x be set ; :: thesis: ( x in { [(k - 1),k] where k is Element of NAT : ( k in y9 & k > i ) } implies ex y, z being set 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 set 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 set ;
take y = y; :: thesis: ex z being set 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
let x be set ; :: 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 RELAT_1:def 4; :: thesis: verum
end;
now
let x be set ; :: 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 set such that
A18: [x,y] in f2 by RELAT_1:def 4;
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, ZFMISC_1:27;
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:1;
A22: now
let x, y1, y2 be set ; :: 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
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 A25: [x,y1] in id { k where k is Element of NAT : ( k in y & k < i ) } ; :: thesis: b2 = b3
then A26: x in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) by RELAT_1:def 4;
then (id { k where k is Element of NAT : ( k in y & k < i ) } ) . x = x by FUNCT_1:17;
then A27: y1 = x by A25, A26, FUNCT_1:def 2;
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 A28: [x,y2] in id { k where k is Element of NAT : ( k in y & k < i ) } ; :: thesis: b2 = b3
then A29: x in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) by RELAT_1:def 4;
then (id { k where k is Element of NAT : ( k in y & k < i ) } ) . x = x by FUNCT_1:17;
hence y1 = y2 by A27, A28, A29, FUNCT_1:def 2; :: thesis: verum
end;
suppose A30: [x,y2] in f2 ; :: thesis: b2 = b3
x in { k where k is Element of NAT : ( k in y & k < i ) } by A26;
then consider k9 being Element of NAT such that
A31: k9 = x and
k9 in y and
A32: k9 < i ;
x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } by A21, A30, RELAT_1:def 4;
then ex k being Element of NAT st
( k - 1 = x & k in y & k > i ) ;
then k9 + 1 > i by A31;
hence y1 = y2 by A32, 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
A33: [(k - 1),k] = [x,y1] and
k in y9 and
A34: k > i ;
A35: k - 1 = x by A33, ZFMISC_1:27;
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 RELAT_1:def 4;
then x in { k where k is Element of NAT : ( k in y & k < i ) } ;
then consider k9 being Element of NAT such that
A36: k9 = x and
k9 in y and
A37: k9 < i ;
k9 = k - 1 by A33, A36, ZFMISC_1:27;
then k9 + 1 > i by A34;
hence y1 = y2 by A37, NAT_1:13; :: thesis: verum
end;
suppose [x,y2] in f2 ; :: thesis: b2 = b3
then consider k9 being Element of NAT such that
A38: [(k9 - 1),k9] = [x,y2] and
k9 in y9 and
k9 > i ;
k9 - 1 = x by A38, ZFMISC_1:27;
hence y1 = y2 by A33, A35, A38, ZFMISC_1:27; :: thesis: verum
end;
end;
end;
end;
end;
A39: now
let x, y1, y2 be set ; :: 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
A40: [(k - 1),k] = [x,y1] and
k in y9 and
k > i ;
A41: k - 1 = x by A40, ZFMISC_1:27;
assume [x,y2] in f2 ; :: thesis: y1 = y2
then consider k9 being Element of NAT such that
A42: [(k9 - 1),k9] = [x,y2] and
k9 in y9 and
k9 > i ;
k9 - 1 = x by A42, ZFMISC_1:27;
hence y1 = y2 by A40, A42, A41, ZFMISC_1:27; :: 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;
A43: now
let x be set ; :: 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 )
A44: 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 RELAT_1:1;
then A45: dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) c= dom f by XBOOLE_1:7;
assume A46: 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 A46, A45, A44, FUNCT_1:def 2; :: thesis: verum
end;
reconsider f2 = f2 as Function by A39, FUNCT_1:def 1;
assume A47: not i in y ; :: thesis: ex x being set st
( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n )
A48: now
let z be set ; :: thesis: ( z in y9 implies b1 in rng f )
set k = z;
assume A49: 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 A47, A49, XXREAL_0:1;
then z in { k where k is Element of NAT : ( k in y & k < i ) } by A49;
then z in rng (id { k where k is Element of NAT : ( k in y & k < i ) } ) by RELAT_1:45;
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 A50: k > i ; :: thesis: b1 in rng f
set x99 = k - 1;
[(k - 1),z] in f2 by A49, A50;
then z in rng f2 by RELAT_1:def 5;
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
let z be set ; :: thesis: ( z in rng f implies b1 in y9 )
assume z in rng f ; :: thesis: b1 in y9
then A51: 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 A51, 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 set such that
A52: [x99,z] in f2 by RELAT_1:def 5;
ex k being Element of NAT st
( [(k - 1),k] = [x99,z] & k in y9 & k > i ) by A52;
hence z in y9 by ZFMISC_1:27; :: thesis: verum
end;
end;
end;
then A53: rng f = y9 by A48, TARSKI:1;
now
let a, b be set ; :: 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 A54: [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 A54, XBOOLE_0:def 3;
suppose A55: [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;
A56: a = b by A55, RELAT_1:def 10;
a in { k where k is Element of NAT : ( k in y & k < i ) } by A55, RELAT_1:def 10;
then consider a9 being Element of NAT such that
A57: a9 = a and
A58: a9 in y and
A59: a9 < i ;
A60: 1 <= a9 by A1, A58, FINSEQ_1:1;
i <= n + 1 by A3, FINSEQ_1:1;
then a9 < n + 1 by A59, XXREAL_0:2;
then a9 <= n by NAT_1:13;
then A61: a in Seg n by A57, A60;
then a in Seg (len (Sgm ((Seg (n + 1)) \ {i}))) by A3, FINSEQ_3:107;
then A62: a in dom (Sgm ((Seg (n + 1)) \ {i})) by FINSEQ_1:def 3;
a9 = (Sgm ((Seg (n9 + 1)) \ {i9})) . a9 by A3, A57, A59, A60, A61, FINSEQ_3:108;
then [a,b] in Sgm ((Seg (n + 1)) \ {i}) by A56, A57, A62, FUNCT_1:1;
hence [a,b] in (rng f) | (Sgm ((Seg (n + 1)) \ {i})) by A53, A56, A57, A58, RELAT_1:def 12; :: thesis: verum
end;
suppose A63: [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
A64: [a,b] = [(b9 - 1),b9] and
A65: b9 in y9 and
A66: b9 > i by A63;
A67: a = b9 - 1 by A64, ZFMISC_1:27;
reconsider a9 = b9 - 1 as integer number ;
i + 1 <= b9 by A66, NAT_1:13;
then A68: (i + 1) - 1 <= b9 - 1 by XREAL_1:9;
then A69: 1 <= a9 by A4, XXREAL_0:2;
reconsider a9 = a9 as Element of NAT by A68, INT_1:3;
b9 <= n + 1 by A1, A65, FINSEQ_1:1;
then A70: b9 - 1 <= (n + 1) - 1 by XREAL_1:9;
then A71: a9 in Seg n by A69;
then a in Seg n by A64, ZFMISC_1:27;
then a in Seg (len (Sgm ((Seg (n + 1)) \ {i}))) by A3, FINSEQ_3:107;
then A72: a in dom (Sgm ((Seg (n + 1)) \ {i})) by FINSEQ_1:def 3;
a9 + 1 = (Sgm ((Seg (n9 + 1)) \ {i9})) . a9 by A3, A70, A68, A71, FINSEQ_3:108;
then [a,b] in Sgm ((Seg (n + 1)) \ {i}) by A64, A67, A72, FUNCT_1:1;
hence [a,b] in (rng f) | (Sgm ((Seg (n + 1)) \ {i})) by A53, A64, A65, RELAT_1:def 12; :: thesis: verum
end;
end;
end;
assume A73: [a,b] in (rng f) | (Sgm ((Seg (n + 1)) \ {i})) ; :: thesis: [b1,b2] in f
then A74: [a,b] in Sgm ((Seg (n + 1)) \ {i}) by RELAT_1:def 12;
then A75: a in dom (Sgm ((Seg (n + 1)) \ {i})) by RELAT_1:def 4;
b in rng f by A73, RELAT_1:def 12;
then b in Seg (n + 1) by A1, A53;
then reconsider a9 = a, b9 = b as Element of NAT by A75;
A76: a in Seg (len (Sgm ((Seg (n + 1)) \ {i}))) by A75, FINSEQ_1:def 3;
then A77: 1 <= a9 by FINSEQ_1:1;
A78: b in y by A53, A73, RELAT_1:def 12;
A79: a in Seg n by A3, A76, FINSEQ_3:107;
reconsider i = i, n = n as Element of NAT by ORDINAL1:def 12;
A80: a9 <= n by A79, FINSEQ_1:1;
per cases ( a9 < i or i <= a9 ) ;
suppose A81: a9 < i ; :: thesis: [b1,b2] in f
then (Sgm ((Seg (n + 1)) \ {i})) . a9 = a9 by A3, A79, A77, FINSEQ_3:108;
then A82: b = a by A74, FUNCT_1:1;
then a9 in { k where k is Element of NAT : ( k in y & k < i ) } by A78, A81;
then [a,b] in id { k where k is Element of NAT : ( k in y & k < i ) } by A82, RELAT_1:def 10;
hence [a,b] in f by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
then A87: f = (rng f) | (Sgm ((Seg (n + 1)) \ {i})) by RELAT_1:def 2;
reconsider g = f " as PartFunc of (dom (f ")),(rng (f ")) by RELSET_1:4;
A88: now
let x be set ; :: thesis: ( x in dom f2 implies f . x = f2 . x )
A89: 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 RELAT_1:1;
then A90: dom f2 c= dom f by XBOOLE_1:7;
assume A91: 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 A91, A90, A89, FUNCT_1:def 2; :: thesis: verum
end;
now
let y1, y2 be set ; :: 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 A92: y1 in (dom (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (dom f2) by RELAT_1:1;
assume y2 in dom f ; :: thesis: ( f . y1 = f . y2 implies b1 = b2 )
then A93: y2 in (dom (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (dom f2) by RELAT_1:1;
assume A94: 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 A92, XBOOLE_0:def 3;
suppose A95: y1 in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) ; :: thesis: b1 = b2
then A96: (id { k where k is Element of NAT : ( k in y & k < i ) } ) . y1 = y1 by FUNCT_1:17;
then A97: f . y1 = y1 by A43, A95;
per cases ( y2 in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) or y2 in dom f2 ) by A93, XBOOLE_0:def 3;
suppose A98: 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 A43, A94, A97, A98; :: thesis: verum
end;
suppose A99: y2 in dom f2 ; :: thesis: b1 = b2
then f . y2 = f2 . y2 by A88;
then [y2,(f . y2)] in f2 by A99, FUNCT_1:def 2;
then A100: 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 A43, A95;
then f . y1 in { k where k is Element of NAT : ( k in y & k < i ) } by A95, A96;
then ex k9 being Element of NAT st
( k9 = f . y1 & k9 in y & k9 < i ) ;
hence y1 = y2 by A94, A100, ZFMISC_1:27; :: thesis: verum
end;
end;
end;
suppose A101: y1 in dom f2 ; :: thesis: b1 = b2
then f . y1 = f2 . y1 by A88;
then [y1,(f . y1)] in f2 by A101, FUNCT_1:def 2;
then consider k being Element of NAT such that
A102: [(k - 1),k] = [y1,(f . y1)] and
k in y9 and
A103: k > i ;
A104: k = f . y1 by A102, ZFMISC_1:27;
per cases ( y2 in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) or y2 in dom f2 ) by A93, XBOOLE_0:def 3;
suppose A105: 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 A43, A105;
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 A94, A102, A103, ZFMISC_1:27; :: thesis: verum
end;
suppose A106: y2 in dom f2 ; :: thesis: b1 = b2
then f . y2 = f2 . y2 by A88;
then [y2,(f . y2)] in f2 by A106, FUNCT_1:def 2;
then consider k being Element of NAT such that
A107: [(k - 1),k] = [y2,(f . y2)] and
k in y9 and
k > i ;
k = f . y2 by A107, ZFMISC_1:27;
hence y1 = y2 by A94, A102, A104, A107, ZFMISC_1:27; :: thesis: verum
end;
end;
end;
end;
end;
then A108: f is one-to-one by FUNCT_1:def 4;
then f " = f ~ by FUNCT_1:def 5;
then A109: f " = ((Sgm ((Seg (n + 1)) \ {i})) ~) | (dom (f ")) by A87, Lm36;
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 ) } by RELAT_1:45;
then A110: dom f = x9 by A21, RELAT_1:1;
then dom f c= NAT by A14, XBOOLE_1:1;
then rng g c= NAT by A108, FUNCT_1:33;
then A111: rng g c= REAL by XBOOLE_1:1;
rng f c= NAT by A1, A53, XBOOLE_1:1;
then dom g c= NAT by A108, FUNCT_1:33;
then dom g c= REAL by XBOOLE_1:1;
then reconsider g = g as PartFunc of REAL,REAL by A111, RELSET_1:7;
A112: dom (f ") = y by A108, A53, FUNCT_1:33;
now
let r1, r2 be Element of REAL ; :: thesis: ( r1 in y /\ (dom g) & r2 in y /\ (dom g) & r1 < r2 implies g . b1 < g . b2 )
A113: g = ((id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2) ~ by A108, 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 A114: [r1,(g . r1)] in g by A112, FUNCT_1:1;
assume r2 in y /\ (dom g) ; :: thesis: ( r1 < r2 implies g . b1 < g . b2 )
then A115: [r2,(g . r2)] in g by A112, FUNCT_1:1;
assume A116: 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 A114, A113, 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 A117: [r1,(g . r1)] in id { k where k is Element of NAT : ( k in y & k < i ) } by RELAT_1:46;
then A118: r1 = g . r1 by RELAT_1:def 10;
r1 in { k where k is Element of NAT : ( k in y & k < i ) } by A117, RELAT_1:def 10;
then A119: ex k9 being Element of NAT st
( g . r1 = k9 & k9 in y & k9 < i ) by A118;
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 A115, A113, 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 ) } by RELAT_1:46;
hence g . r1 < g . r2 by A116, A118, 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
A120: [(k99 - 1),k99] = [(g . r2),r2] and
k99 in y9 and
A121: k99 > i ;
reconsider k999 = g . r2, i9 = i - 1 as integer number by A120, ZFMISC_1:27;
k99 - 1 = g . r2 by A120, ZFMISC_1:27;
then i - 1 < g . r2 by A121, XREAL_1:9;
then i9 + 1 <= k999 by INT_1:7;
hence g . r1 < g . r2 by A119, 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
A122: [(k9 - 1),k9] = [(g . r1),r1] and
k9 in y9 and
A123: k9 > i ;
A124: k9 - 1 = g . r1 by A122, ZFMISC_1:27;
A125: r1 = k9 by A122, ZFMISC_1:27;
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 A115, A113, 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 ) } by RELAT_1:46;
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 A116, A123, A125, 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
A126: [(k99 - 1),k99] = [(g . r2),r2] and
k99 in y9 and
k99 > i ;
( k99 - 1 = g . r2 & r2 = k99 ) by A126, ZFMISC_1:27;
hence g . r1 < g . r2 by A116, A124, A125, XREAL_1:9; :: thesis: verum
end;
end;
end;
end;
end;
then A127: g | y is increasing by RFUNCT_2:20;
A128: 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 A108, A110, FUNCT_1:33;
then A129: { 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 A112, RELAT_1:113;
now
let x9 be set ; :: thesis: ( x9 in g .: y implies x9 in NAT \ {0} )
assume A130: x9 in g .: y ; :: thesis: x9 in NAT \ {0}
then not x9 = 0 by A14, A129, FINSEQ_1:1;
then A131: not x9 in {0} by TARSKI:def 1;
x9 in Seg n by A6, A129, A130;
hence x9 in NAT \ {0} by A131, XBOOLE_0:def 5; :: thesis: verum
end;
then A132: g .: y c= NAT \ {0} by TARSKI:def 3;
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, XBOOLE_1:36;
then A133: (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 A112, A128, RELAT_1:113
.= (((Sgm ((Seg (n + 1)) \ {i})) ") | y) * (Sgm y) by A1, A112, A127, A132, A133, A109, Lm38
.= ((Sgm ((Seg (n + 1)) \ {i})) ") * (y | (Sgm y)) by Lm37
.= ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) by A2, RELAT_1:95 ;
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, TARSKI:def 3; :: thesis: verum