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 }

proof

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 }

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 } ) )

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

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;

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

then x = f . n by TARSKI:def 1;
hence x in { (f . k1) where k1 is Nat : n <= k1 } ; :: thesis: verum

end;

end;

end;

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

end;

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

proof

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;

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