let N be Element of NAT ; :: thesis: for r being Real
for seq being Real_Sequence of N st r <> 0 & seq is non-zero holds
r * seq is non-zero
let r be Real; :: thesis: for seq being Real_Sequence of N st r <> 0 & seq is non-zero holds
r * seq is non-zero
let seq be Real_Sequence of N; :: thesis: ( r <> 0 & seq is non-zero implies r * seq is non-zero )
assume that
A1: r <> 0 and
A2: seq is non-zero and
A3: not r * seq is non-zero ; :: thesis: contradiction
consider n1 being Element of NAT such that
A4: (r * seq) . n1 = 0. (TOP-REAL N) by A3, Th4;
A5: seq . n1 <> 0. (TOP-REAL N) by A2, Th4;
r * (seq . n1) = 0. (TOP-REAL N) by A4, LmDef3;
hence contradiction by A1, A5, EUCLID:31; :: thesis: verum