let X be set ; :: thesis: for i being Nat st X c= Seg i & 1 in X holds
(Sgm X) . 1 = 1
let i be Nat; :: thesis: ( X c= Seg i & 1 in X implies (Sgm X) . 1 = 1 )
assume that
A1: X c= Seg i and
A2: 1 in X ; :: thesis: (Sgm X) . 1 = 1
A3: rng (Sgm X) = X by A1, FINSEQ_1:def 13;
then consider x being set such that
A4: x in dom (Sgm X) and
A5: (Sgm X) . x = 1 by A2, FUNCT_1:def 5;
reconsider j = x as Element of NAT by A4;
A6: j >= 1 by A4, FINSEQ_3:27;
A7: rng (Sgm X) c= NAT by FINSEQ_1:def 4;
assume A8: (Sgm X) . 1 <> 1 ; :: thesis: contradiction
Sgm X <> {} by A1, A2, FINSEQ_1:72;
then len (Sgm X) <> 0 ;
then len (Sgm X) >= 1 by NAT_1:14;
then 1 in dom (Sgm X) by FINSEQ_3:27;
then A9: ( (Sgm X) . 1 in rng (Sgm X) & (Sgm X) . j in rng (Sgm X) ) by A4, FUNCT_1:def 5;
then reconsider k1 = (Sgm X) . 1 as Element of NAT by A7;
A10: k1 >= 1 by A1, A3, A9, FINSEQ_1:3;
A11: j <= len (Sgm X) by A4, FINSEQ_3:27;
1 < j by A5, A6, A8, XXREAL_0:1;
hence contradiction by A1, A5, A10, A11, FINSEQ_1:def 13; :: thesis: verum