let seq, seq1 be Real_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 A1: ( seq is non-zero & seq1 is non-zero ) ; :: thesis: seq (#) seq1 is non-zero
now :: thesis: for n being Nat holds (seq (#) seq1) . n <> 0
let n be Nat; :: thesis: (seq (#) seq1) . n <> 0
A2: (seq (#) seq1) . n = (seq . n) * (seq1 . n) by Th8;
( seq . n <> 0 & seq1 . n <> 0 ) by ;
hence (seq (#) seq1) . n <> 0 by ; :: thesis: verum
end;
hence seq (#) seq1 is non-zero by Th5; :: thesis: verum
end;
assume A3: seq (#) seq1 is non-zero ; :: thesis: ( seq is non-zero & seq1 is non-zero )
now :: thesis: for n being Nat holds seq . n <> 0
let n be Nat; :: thesis: seq . n <> 0
(seq (#) seq1) . n = (seq . n) * (seq1 . n) by Th8;
hence seq . n <> 0 by ; :: thesis: verum
end;
hence seq is non-zero by Th5; :: thesis: seq1 is non-zero
now :: thesis: for n being Nat holds seq1 . n <> 0
let n be Nat; :: thesis: seq1 . n <> 0
(seq (#) seq1) . n = (seq . n) * (seq1 . n) by Th8;
hence seq1 . n <> 0 by ; :: thesis: verum
end;
hence seq1 is non-zero by Th5; :: thesis: verum