let X be included_in_Seg set ; ( 1 in X implies (Sgm X) . 1 = 1 )
assume A2:
1 in X
; (Sgm X) . 1 = 1
Sgm X <> {}
by A2, FINSEQ_1:51;
then
len (Sgm X) >= 1
by NAT_1:14;
then
1 in dom (Sgm X)
by FINSEQ_3:25;
then A3:
(Sgm X) . 1 in rng (Sgm X)
by FUNCT_1:def 3;
reconsider k1 = (Sgm X) . 1 as Nat ;
assume A4:
(Sgm X) . 1 <> 1
; contradiction
A5:
rng (Sgm X) = X
by FINSEQ_1:def 14;
then consider x being object such that
A6:
x in dom (Sgm X)
and
A7:
(Sgm X) . x = 1
by A2, FUNCT_1:def 3;
ex k being Nat st X c= Seg k
by FINSEQ_1:def 13;
then A8:
k1 >= 1
by A5, A3, FINSEQ_1:1;
reconsider j = x as Nat by A6;
j >= 1
by A6, FINSEQ_3:25;
then A9:
1 < j
by A7, A4, XXREAL_0:1;
j <= len (Sgm X)
by A6, FINSEQ_3:25;
hence
contradiction
by A7, A8, A9, FINSEQ_1:def 14; verum