let X be set ; for i being Nat st X c= Seg i & 1 in X holds
(Sgm X) . 1 = 1
let i be Nat; ( X c= Seg i & 1 in X implies (Sgm X) . 1 = 1 )
assume that
A1:
X c= Seg i
and
A2:
1 in X
; (Sgm X) . 1 = 1
Sgm X <> {}
by A1, 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 A1, FINSEQ_1:def 13;
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;
A8:
k1 >= 1
by A1, 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 A1, A7, A8, A9, FINSEQ_1:def 13; verum