let X be set ; :: thesis: for k being Nat st X c= Seg k holds

rng (Sgm X) c= Seg k

let k be Nat; :: thesis: ( X c= Seg k implies rng (Sgm X) c= Seg k )

assume A1: X c= Seg k ; :: thesis: rng (Sgm X) c= Seg k

for x being object st x in rng (Sgm X) holds

x in Seg k

rng (Sgm X) c= Seg k

let k be Nat; :: thesis: ( X c= Seg k implies rng (Sgm X) c= Seg k )

assume A1: X c= Seg k ; :: thesis: rng (Sgm X) c= Seg k

for x being object st x in rng (Sgm X) holds

x in Seg k

proof

hence
rng (Sgm X) c= Seg k
; :: thesis: verum
let x be object ; :: thesis: ( x in rng (Sgm X) implies x in Seg k )

assume A2: x in rng (Sgm X) ; :: thesis: x in Seg k

rng (Sgm X) = X by A1, FINSEQ_1:def 13;

hence x in Seg k by A1, A2; :: thesis: verum

end;assume A2: x in rng (Sgm X) ; :: thesis: x in Seg k

rng (Sgm X) = X by A1, FINSEQ_1:def 13;

hence x in Seg k by A1, A2; :: thesis: verum