let n be Element of NAT ; :: thesis: for Y being set
for f being Function of NAT ,Y holds { (f . k1) where k1 is Element of NAT : n <= k1 } = { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)}
let Y be set ; :: thesis: for f being Function of NAT ,Y holds { (f . k1) where k1 is Element of NAT : n <= k1 } = { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)}
let f be Function of NAT ,Y; :: thesis: { (f . k1) where k1 is Element of NAT : n <= k1 } = { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)}
set Z1 = { (f . k1) where k1 is Element of NAT : n <= k1 } ;
set Z2 = { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } ;
A00: { (f . k1) where k1 is Element of NAT : n <= k1 } c= { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f . k1) where k1 is Element of NAT : n <= k1 } or x in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} )
assume x in { (f . k1) where k1 is Element of NAT : n <= k1 } ; :: thesis: x in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)}
then consider z being set such that
B0: ( x = z & z in { (f . k1) where k1 is Element of NAT : n <= k1 } ) ;
consider k being Element of NAT such that
B1: ( z = f . k & n <= k ) by B0;
( ( z = f . k & n + 1 <= k ) or ( z = f . k & n = k ) ) by B1, LM1;
then ( z in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } or z in {(f . n)} ) by TARSKI:def 1;
hence x in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} by B0, XBOOLE_0:def 3; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} or x in { (f . k1) where k1 is Element of NAT : n <= k1 } )
assume C0: x in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} ; :: thesis: x in { (f . k1) where k1 is Element of NAT : n <= k1 }

now

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

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

then consider z being set such that
CA2: ( x = z & z in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } ) ;
consider k11 being Element of NAT such that
CA3: ( z = f . k11 & n + 1 <= k11 ) by CA2;
n <= k11 by CA3, NAT_1:13;
hence x in { (f . k1) where k1 is Element of NAT : n <= k1 } by CA2, CA3; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

hence { (f . k1) where k1 is Element of NAT : n <= k1 } = { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} by A00, XBOOLE_0:def 10; :: thesis: verum