set p = ProdFinSeq X;
defpred S₁[ Nat] means ( m < len (ProdFinSeq X) implies (ProdFinSeq X) . (m + 1) <> {} );
dom (ProdFinSeq X) = Seg m by FINSEQ_1:89;
then A0: Seg (len (ProdFinSeq X)) = Seg m by FINSEQ_1:def 3;
A2: ( (ProdFinSeq X) . 1 = X . 1 & ( for i being non zero Nat st i < m holds
(ProdFinSeq X) . (i + 1) = [:((ProdFinSeq X) . i),(X . (i + 1)):] ) ) by Def3;
1 <= len X by NAT_1:14;
then 1 in dom X by FINSEQ_3:25;
then A3: S₁[ 0 ] by A2;
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
assume A6: i + 1 < len (ProdFinSeq X) ; :: thesis: (ProdFinSeq X) . ((i + 1) + 1) <> {}
then ( 1 <= (i + 1) + 1 & (i + 1) + 1 <= len (ProdFinSeq X) ) by NAT_1:13, NAT_1:14;
then (i + 1) + 1 in Seg m by A0;
then A7: (i + 1) + 1 in dom X by FINSEQ_1:89;
len (ProdFinSeq X) = m by A0, FINSEQ_1:6;
then (ProdFinSeq X) . ((i + 1) + 1) = [:((ProdFinSeq X) . (i + 1)),(X . ((i + 1) + 1)):] by A6, Def3;
hence (ProdFinSeq X) . ((i + 1) + 1) <> {} by A5, A6, A7, NAT_1:12; :: thesis: verum

end;

A8: for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
for i being object st i in dom (ProdFinSeq X) holds
(ProdFinSeq X) . i <> {}

proof

let i be object ; :: thesis: ( i in dom (ProdFinSeq X) implies (ProdFinSeq X) . i <> {} )
assume A9: i in dom (ProdFinSeq X) ; :: thesis: (ProdFinSeq X) . i <> {}
then reconsider j = i as Nat ;
reconsider j1 = j - 1 as Nat by A9, FINSEQ_3:25, NAT_1:21;
j1 + 1 <= len (ProdFinSeq X) by A9, FINSEQ_3:25;
hence (ProdFinSeq X) . i <> {} by A8, NAT_1:13; :: thesis: verum

end;

hence ProdFinSeq X is non-empty ; :: thesis: verum