let p be XFinSequence of NAT ; :: thesis: ( p is dominated_by_0 implies p . 0 = 0 )
assume A1: p is dominated_by_0 ; :: thesis: p . 0 = 0

now :: thesis: p . 0 = 0

per cases ( not 0 in dom p or 0 in dom p ) ;

suppose not 0 in dom p ; :: thesis: p . 0 = 0

hence p . 0 = 0 by FUNCT_1:def 2; :: thesis: verum

end;

suppose 0 in dom p ; :: thesis: p . 0 = 0

then len p >= 1 by NAT_1:14;
then A2: Segm 1 c= Segm (len p) by NAT_1:39;
0 in Segm 1 by NAT_1:44;
then 0 in (dom p) /\ (Segm 1) by A2, XBOOLE_0:def 4;
then A3: (p | 1) . 0 = p . 0 by FUNCT_1:48;
A4: Sum <%(p . 0)%> = addnat "**" <%(p . 0)%> by AFINSQ_2:51
.= p . 0 by AFINSQ_2:37 ;
len (p | 1) = 1 by A2, RELAT_1:62;
then p | 1 = <%(p . 0)%> by A3, AFINSQ_1:34;
then 2 * (p . 0) <= 1 + 0 by A1, A4, Th2;
then ( 2 * (p . 0) = 1 or 2 * (p . 0) = 0 ) by NAT_1:9;
hence p . 0 = 0 by NAT_1:15; :: thesis: verum

end;

end;

end;

hence p . 0 = 0 ; :: thesis: verum