let seq, seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is non-zero implies seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1) )
assume A1: seq1 is non-zero ; :: thesis: seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1)
now :: thesis: for n being Element of NAT holds (seq2 /" seq) . n = ((seq2 (#) seq1) /" (seq (#) seq1)) . n
let n be Element of NAT ; :: thesis: (seq2 /" seq) . n = ((seq2 (#) seq1) /" (seq (#) seq1)) . n
A2: seq1 . n <> 0 by ;
thus (seq2 /" seq) . n = ((seq2 . n) * 1) * ((seq ") . n) by Th8
.= ((seq2 . n) * ((seq1 . n) * ((seq1 . n) "))) * ((seq ") . n) by
.= ((seq2 . n) * (seq1 . n)) * (((seq1 . n) ") * ((seq ") . n))
.= ((seq2 (#) seq1) . n) * (((seq1 . n) ") * ((seq ") . n)) by Th8
.= ((seq2 (#) seq1) . n) * (((seq1 ") . n) * ((seq ") . n)) by VALUED_1:10
.= ((seq2 (#) seq1) . n) * (((seq ") (#) (seq1 ")) . n) by Th8
.= ((seq2 (#) seq1) . n) * (((seq (#) seq1) ") . n) by Th34
.= ((seq2 (#) seq1) /" (seq (#) seq1)) . n by Th8 ; :: thesis: verum
end;
hence seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1) by FUNCT_2:63; :: thesis: verum