let x be set ; :: 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 EUCLID:3;
A2: dom ((0.REAL n) +* (x,0)) = dom (0.REAL n) by FUNCT_7:32;
A3: dom (0.REAL n) = Seg n by EUCLID:3;

now

let z be set ; :: 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:33
.= (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:34; :: thesis: verum

end;

end;

end;

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