let L be non empty ZeroStr ; :: thesis: <%(0. L),(0. L)%> = 0_. L
0 is_at_least_length_of <%(0. L),(0. L)%>
proof
let n be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not 0 <= n or <%(0. L),(0. L)%> . n = 0. L )
assume n >= 0 ; :: thesis: <%(0. L),(0. L)%> . n = 0. L
per cases ( n = 0 or n > 0 ) ;
suppose n = 0 ; :: thesis: <%(0. L),(0. L)%> . n = 0. L
hence <%(0. L),(0. L)%> . n = 0. L by Th38; :: thesis: verum
end;
suppose n > 0 ; :: thesis: <%(0. L),(0. L)%> . n = 0. L
then A1: n >= 0 + 1 by NAT_1:13;
now :: thesis: <%(0. L),(0. L)%> . n = 0. L
per cases ( n = 1 or n > 1 ) by A1, XXREAL_0:1;
suppose n = 1 ; :: thesis: <%(0. L),(0. L)%> . n = 0. L
hence <%(0. L),(0. L)%> . n = 0. L by Th38; :: thesis: verum
end;
suppose n > 1 ; :: thesis: <%(0. L),(0. L)%> . n = 0. L
then n >= 1 + 1 by NAT_1:13;
hence <%(0. L),(0. L)%> . n = 0. L by Th38; :: thesis: verum
end;
end;
end;
hence <%(0. L),(0. L)%> . n = 0. L ; :: thesis: verum
end;
end;
end;
then len <%(0. L),(0. L)%> = 0 by ALGSEQ_1:def 3;
hence <%(0. L),(0. L)%> = 0_. L by POLYNOM4:5; :: thesis: verum