let seq1, seq2 be Real_Sequence; :: thesis: for Ns being increasing sequence of NAT holds
( (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) & (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) )
let Ns be increasing sequence of NAT; :: thesis: ( (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) & (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) )

now :: thesis: for n being Element of NAT holds ((seq1 + seq2) * Ns) . n = ((seq1 * Ns) + (seq2 * Ns)) . n

let n be Element of NAT ; :: thesis: ((seq1 + seq2) * Ns) . n = ((seq1 * Ns) + (seq2 * Ns)) . n
thus ((seq1 + seq2) * Ns) . n = (seq1 + seq2) . (Ns . n) by FUNCT_2:15
.= (seq1 . (Ns . n)) + (seq2 . (Ns . n)) by SEQ_1:7
.= ((seq1 * Ns) . n) + (seq2 . (Ns . n)) by FUNCT_2:15
.= ((seq1 * Ns) . n) + ((seq2 * Ns) . n) by FUNCT_2:15
.= ((seq1 * Ns) + (seq2 * Ns)) . n by SEQ_1:7 ; :: thesis: verum

end;

hence (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) by FUNCT_2:63; :: thesis: ( (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) )

now :: thesis: for n being Element of NAT holds ((seq1 - seq2) * Ns) . n = ((seq1 * Ns) - (seq2 * Ns)) . n

let n be Element of NAT ; :: thesis: ((seq1 - seq2) * Ns) . n = ((seq1 * Ns) - (seq2 * Ns)) . n
thus ((seq1 - seq2) * Ns) . n = (seq1 - seq2) . (Ns . n) by FUNCT_2:15
.= (seq1 . (Ns . n)) - (seq2 . (Ns . n)) by Th1
.= ((seq1 * Ns) . n) - (seq2 . (Ns . n)) by FUNCT_2:15
.= ((seq1 * Ns) . n) - ((seq2 * Ns) . n) by FUNCT_2:15
.= ((seq1 * Ns) - (seq2 * Ns)) . n by Th1 ; :: thesis: verum

end;

hence (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) by FUNCT_2:63; :: thesis: (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns)

now :: thesis: for n being Element of NAT holds ((seq1 (#) seq2) * Ns) . n = ((seq1 * Ns) (#) (seq2 * Ns)) . n

let n be Element of NAT ; :: thesis: ((seq1 (#) seq2) * Ns) . n = ((seq1 * Ns) (#) (seq2 * Ns)) . n
thus ((seq1 (#) seq2) * Ns) . n = (seq1 (#) seq2) . (Ns . n) by FUNCT_2:15
.= (seq1 . (Ns . n)) * (seq2 . (Ns . n)) by SEQ_1:8
.= ((seq1 * Ns) . n) * (seq2 . (Ns . n)) by FUNCT_2:15
.= ((seq1 * Ns) . n) * ((seq2 * Ns) . n) by FUNCT_2:15
.= ((seq1 * Ns) (#) (seq2 * Ns)) . n by SEQ_1:8 ; :: thesis: verum

end;

hence (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) by FUNCT_2:63; :: thesis: verum