let seq, seq1 be Complex_Sequence; :: thesis: ( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero )
thus ( seq is non-zero & seq1 is non-zero implies seq (#) seq1 is non-zero ) :: thesis: ( seq (#) seq1 is non-zero implies ( seq is non-zero & seq1 is non-zero ) )

proof

assume that
A1: seq is non-zero and
A2: seq1 is non-zero ; :: thesis: seq (#) seq1 is non-zero

now

let n be Element of NAT ; :: thesis: (seq (#) seq1) . n <> 0c
A3: seq . n <> 0c by A1, Th4;
A4: seq1 . n <> 0c by A2, Th4;
(seq (#) seq1) . n = (seq . n) * (seq1 . n) by VALUED_1:5;
hence (seq (#) seq1) . n <> 0c by A3, A4; :: thesis: verum

end;

hence seq (#) seq1 is non-zero by Th4; :: thesis: verum

end;

assume A5: seq (#) seq1 is non-zero ; :: thesis: ( seq is non-zero & seq1 is non-zero )

now

let n be Element of NAT ; :: thesis: seq . n <> 0c
(seq (#) seq1) . n = (seq . n) * (seq1 . n) by VALUED_1:5;
hence seq . n <> 0c by A5, Th4; :: thesis: verum

end;

hence seq is non-zero by Th4; :: thesis: seq1 is non-zero

now

let n be Element of NAT ; :: thesis: seq1 . n <> 0c
(seq (#) seq1) . n = (seq . n) * (seq1 . n) by VALUED_1:5;
hence seq1 . n <> 0c by A5, Th4; :: thesis: verum

end;

hence seq1 is non-zero by Th4; :: thesis: verum