take 2 ; :: according to ALGSEQ_1:def 1 :: thesis: for b₁ being set holds
( not 2 <= b₁ or <%z0,z1%> . b₁ = 0. L )
let n be Nat; :: thesis: ( not 2 <= n or <%z0,z1%> . n = 0. L )
thus ( not 2 <= n or <%z0,z1%> . n = 0. L ) by Th38; :: thesis: verum