let L be non empty ZeroStr ; :: thesis: (0. L) | L = 0_. L
set p = (0. L) | L;

A2: now :: thesis: for x being object st x in dom ((0. L) | L) holds
((0. L) | L) . x = 0. L

let x be object ; :: thesis: ( x in dom ((0. L) | L) implies ((0. L) | L) . b₁ = 0. L )
assume x in dom ((0. L) | L) ; :: thesis: ((0. L) | L) . b₁ = 0. L
then reconsider i = x as Element of NAT ;

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: ((0. L) | L) . b₁ = 0. L

hence ((0. L) | L) . x = 0. L by Th28; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: ((0. L) | L) . b₁ = 0. L

hence ((0. L) | L) . x = 0. L by Th28; :: thesis: verum

end;

end;

end;

dom ((0. L) | L) = NAT by NORMSP_1:12;
hence (0. L) | L = 0_. L by A2, FUNCOP_1:11; :: thesis: verum