let k be Nat; :: thesis: for p being XFinSequence of NAT st p is dominated_by_0 & 2 * (Sum (p | k)) = k holds
( k <= len p & len (p | k) = k )
let p be XFinSequence of NAT ; :: thesis: ( p is dominated_by_0 & 2 * (Sum (p | k)) = k implies ( k <= len p & len (p | k) = k ) )
assume A1: ( p is dominated_by_0 & 2 * (Sum (p | k)) = k ) ; :: thesis: ( k <= len p & len (p | k) = k )
A2: k <= len p

proof

A3: p | (len p) = p ;
assume A4: k > len p ; :: thesis: contradiction
then Segm (len p) c= Segm k by NAT_1:39;
then p | k = p by RELAT_1:68;
hence contradiction by A1, A4, A3; :: thesis: verum

end;

then Segm k c= Segm (len p) by NAT_1:39;
then (dom p) /\ k = k by XBOOLE_1:28;
hence ( k <= len p & len (p | k) = k ) by A2, RELAT_1:61; :: thesis: verum