let r be Real; :: thesis: for seq being Real_Sequence st r <> 0 & seq is non-zero holds

r (#) seq is non-zero

let seq be Real_Sequence; :: 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 Nat such that

A4: (r (#) seq) . n1 = 0 by A3, Th5;

A5: seq . n1 <> 0 by A2, Th5;

r * (seq . n1) = 0 by A4, Th9;

hence contradiction by A1, A5, XCMPLX_1:6; :: thesis: verum

r (#) seq is non-zero

let seq be Real_Sequence; :: 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 Nat such that

A4: (r (#) seq) . n1 = 0 by A3, Th5;

A5: seq . n1 <> 0 by A2, Th5;

r * (seq . n1) = 0 by A4, Th9;

hence contradiction by A1, A5, XCMPLX_1:6; :: thesis: verum