let x be object ; :: thesis: for n being Nat holds (0.REAL n) +* (x,0) = 0.REAL n
let n be Nat; :: thesis: (0.REAL n) +* (x,0) = 0.REAL n
set p = (0.REAL n) +* (x,0);
A1: dom ((0.REAL n) +* (x,0)) = Seg n by FINSEQ_1:89;
A2: dom ((0.REAL n) +* (x,0)) = dom (0.REAL n) by FUNCT_7:30;
A3: dom (0.REAL n) = Seg n ;

now :: thesis: for z being object st z in dom ((0.REAL n) +* (x,0)) holds
((0.REAL n) +* (x,0)) . z = (0.REAL n) . z

let z be object ; :: thesis: ( z in dom ((0.REAL n) +* (x,0)) implies ((0.REAL n) +* (x,0)) . b₁ = (0.REAL n) . b₁ )
assume A4: z in dom ((0.REAL n) +* (x,0)) ; :: thesis: ((0.REAL n) +* (x,0)) . b₁ = (0.REAL n) . b₁

per cases ( z = x or z <> x ) ;

suppose z = x ; :: thesis: ((0.REAL n) +* (x,0)) . b₁ = (0.REAL n) . b₁

hence ((0.REAL n) +* (x,0)) . z = 0 by A1, A3, A4, FUNCT_7:31
.= (0.REAL n) . z ;
:: thesis: verum

end;

suppose z <> x ; :: thesis: ((0.REAL n) +* (x,0)) . b₁ = (0.REAL n) . b₁

hence ((0.REAL n) +* (x,0)) . z = (0.REAL n) . z by FUNCT_7:32; :: thesis: verum

end;

end;

end;

hence (0.REAL n) +* (x,0) = 0.REAL n by A2; :: thesis: verum