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

now

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

end;

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

then len p >= 1 by NAT_1:14;
then A2: 1 c= len p by NAT_1:40;
0 in 1 by NAT_1:45;
then 0 in (dom p) /\ 1 by A2, XBOOLE_0:def 4;
then A3: (p | 1) . 0 = p . 0 by FUNCT_1:71;
A4: Sum <%(p . 0 )%> = addnat "**" <%(p . 0 )%> by AFINSQ_2:63
.= p . 0 by AFINSQ_2:49 ;
len (p | 1) = 1 by A2, RELAT_1:91;
then p | 1 = <%(p . 0 )%> by A3, AFINSQ_1:38;
then 2 * (p . 0 ) <= 1 + 0 by A1, A4, Th6;
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