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