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