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)) . b1 = (0.REAL n) . b1 )
assume A4: z in dom ((0.REAL n) +* (x,0)) ; :: thesis: ((0.REAL n) +* (x,0)) . b1 = (0.REAL n) . b1
per cases ( z = x or z <> x ) ;
suppose z = x ; :: thesis: ((0.REAL n) +* (x,0)) . b1 = (0.REAL n) . b1
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)) . b1 = (0.REAL n) . b1
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