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:72;
then
len (Sgm X) >= 1
by NAT_1:14;
then
1 in dom (Sgm X)
by FINSEQ_3:27;
then A3:
(Sgm X) . 1 in rng (Sgm X)
by FUNCT_1:def 5;
rng (Sgm X) c= NAT
by FINSEQ_1:def 4;
then reconsider k1 = (Sgm X) . 1 as Element of NAT by A3;
assume A4:
(Sgm X) . 1 <> 1
; contradiction
A5:
rng (Sgm X) = X
by A1, FINSEQ_1:def 13;
then consider x being set such that
A6:
x in dom (Sgm X)
and
A7:
(Sgm X) . x = 1
by A2, FUNCT_1:def 5;
A8:
k1 >= 1
by A1, A5, A3, FINSEQ_1:3;
reconsider j = x as Element of NAT by A6;
j >= 1
by A6, FINSEQ_3:27;
then A9:
1 < j
by A7, A4, XXREAL_0:1;
j <= len (Sgm X)
by A6, FINSEQ_3:27;
hence
contradiction
by A1, A7, A8, A9, FINSEQ_1:def 13; verum