let r be Complex; :: thesis: for seq being Complex_Sequence st r <> 0c & seq is non-zero holds
r (#) seq is non-zero
let seq be Complex_Sequence; :: thesis: ( r <> 0c & seq is non-zero implies r (#) seq is non-zero )
assume that
A1: r <> 0c 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 = 0c by A3, Th4;
A5: r * (seq . n1) = 0c by A4, VALUED_1:6;
seq . n1 <> 0c by A2, Th4;
hence contradiction by A1, A5; :: thesis: verum