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 ) )

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 A3:
seq (#) seq1 is non-zero
; :: thesis: ( seq is non-zero & seq1 is non-zero )
assume A1:
( seq is non-zero & seq1 is non-zero )
; :: thesis: seq (#) seq1 is non-zero

end;now :: thesis: for n being Element of NAT holds (seq (#) seq1) . n <> 0c

hence
seq (#) seq1 is non-zero
by Th4; :: thesis: verumlet n be Element of NAT ; :: thesis: (seq (#) seq1) . n <> 0c

A2: (seq (#) seq1) . n = (seq . n) * (seq1 . n) by VALUED_1:5;

( seq . n <> 0c & seq1 . n <> 0c ) by A1, Th4;

hence (seq (#) seq1) . n <> 0c by A2; :: thesis: verum

end;A2: (seq (#) seq1) . n = (seq . n) * (seq1 . n) by VALUED_1:5;

( seq . n <> 0c & seq1 . n <> 0c ) by A1, Th4;

hence (seq (#) seq1) . n <> 0c by A2; :: thesis: verum

now :: thesis: for n being Element of NAT holds seq . n <> 0c

hence
seq is non-zero
by Th4; :: thesis: seq1 is non-zero 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 A3, Th4; :: thesis: verum

end;(seq (#) seq1) . n = (seq . n) * (seq1 . n) by VALUED_1:5;

hence seq . n <> 0c by A3, Th4; :: thesis: verum

now :: thesis: for n being Element of NAT holds seq1 . n <> 0c

hence
seq1 is non-zero
by Th4; :: thesis: verumlet 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 A3, Th4; :: thesis: verum

end;(seq (#) seq1) . n = (seq . n) * (seq1 . n) by VALUED_1:5;

hence seq1 . n <> 0c by A3, Th4; :: thesis: verum