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

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 ; :: thesis: 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; :: thesis: verum

(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

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 ; :: thesis: 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; :: thesis: verum