let n be Nat; :: thesis: for Y being set

for f being sequence of Y holds { (f . k1) where k1 is Nat : n <= k1 } = { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)}

let Y be set ; :: thesis: for f being sequence of Y holds { (f . k1) where k1 is Nat : n <= k1 } = { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)}

let f be sequence of Y; :: thesis: { (f . k1) where k1 is Nat : n <= k1 } = { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)}

set Z1 = { (f . k1) where k1 is Nat : n <= k1 } ;

set Z2 = { (f . k2) where k2 is Nat : n + 1 <= k2 } ;

A1: { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)} c= { (f . k1) where k1 is Nat : n <= k1 }

for f being sequence of Y holds { (f . k1) where k1 is Nat : n <= k1 } = { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)}

let Y be set ; :: thesis: for f being sequence of Y holds { (f . k1) where k1 is Nat : n <= k1 } = { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)}

let f be sequence of Y; :: thesis: { (f . k1) where k1 is Nat : n <= k1 } = { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)}

set Z1 = { (f . k1) where k1 is Nat : n <= k1 } ;

set Z2 = { (f . k2) where k2 is Nat : n + 1 <= k2 } ;

A1: { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)} c= { (f . k1) where k1 is Nat : n <= k1 }

proof

{ (f . k1) where k1 is Nat : n <= k1 } c= { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)} or x in { (f . k1) where k1 is Nat : n <= k1 } )

assume A2: x in { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)} ; :: thesis: x in { (f . k1) where k1 is Nat : n <= k1 }

end;assume A2: x in { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)} ; :: thesis: x in { (f . k1) where k1 is Nat : n <= k1 }

now :: thesis: ( ( x in { (f . k2) where k2 is Nat : n + 1 <= k2 } & x in { (f . k1) where k1 is Nat : n <= k1 } ) or ( x in {(f . n)} & x in { (f . k1) where k1 is Nat : n <= k1 } ) )end;

hence
x in { (f . k1) where k1 is Nat : n <= k1 }
; :: thesis: verumper cases
( x in { (f . k2) where k2 is Nat : n + 1 <= k2 } or x in {(f . n)} )
by A2, XBOOLE_0:def 3;

end;

case
x in { (f . k2) where k2 is Nat : n + 1 <= k2 }
; :: thesis: x in { (f . k1) where k1 is Nat : n <= k1 }

then consider z being object such that

A3: x = z and

A4: z in { (f . k2) where k2 is Nat : n + 1 <= k2 } ;

consider k11 being Nat such that

A5: z = f . k11 and

A6: n + 1 <= k11 by A4;

n <= k11 by A6, NAT_1:13;

hence x in { (f . k1) where k1 is Nat : n <= k1 } by A3, A5; :: thesis: verum

end;A3: x = z and

A4: z in { (f . k2) where k2 is Nat : n + 1 <= k2 } ;

consider k11 being Nat such that

A5: z = f . k11 and

A6: n + 1 <= k11 by A4;

n <= k11 by A6, NAT_1:13;

hence x in { (f . k1) where k1 is Nat : n <= k1 } by A3, A5; :: thesis: verum

proof

hence
{ (f . k1) where k1 is Nat : n <= k1 } = { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)}
by A1, XBOOLE_0:def 10; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f . k1) where k1 is Nat : n <= k1 } or x in { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)} )

assume x in { (f . k1) where k1 is Nat : n <= k1 } ; :: thesis: x in { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)}

then consider z being object such that

A7: x = z and

A8: z in { (f . k1) where k1 is Nat : n <= k1 } ;

consider k being Nat such that

A9: ( z = f . k & n <= k ) by A8;

( ( z = f . k & n + 1 <= k ) or ( z = f . k & n = k ) ) by A9, Lm1;

then ( z in { (f . k2) where k2 is Nat : n + 1 <= k2 } or z in {(f . n)} ) by TARSKI:def 1;

hence x in { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)} by A7, XBOOLE_0:def 3; :: thesis: verum

end;assume x in { (f . k1) where k1 is Nat : n <= k1 } ; :: thesis: x in { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)}

then consider z being object such that

A7: x = z and

A8: z in { (f . k1) where k1 is Nat : n <= k1 } ;

consider k being Nat such that

A9: ( z = f . k & n <= k ) by A8;

( ( z = f . k & n + 1 <= k ) or ( z = f . k & n = k ) ) by A9, Lm1;

then ( z in { (f . k2) where k2 is Nat : n + 1 <= k2 } or z in {(f . n)} ) by TARSKI:def 1;

hence x in { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)} by A7, XBOOLE_0:def 3; :: thesis: verum