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