let seq1, seq2 be Real_Sequence; :: thesis: for Ns being V33() 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 V33() 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

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:21
.= (seq1 . (Ns . n)) + (seq2 . (Ns . n)) by SEQ_1:11
.= ((seq1 * Ns) . n) + (seq2 . (Ns . n)) by FUNCT_2:21
.= ((seq1 * Ns) . n) + ((seq2 * Ns) . n) by FUNCT_2:21
.= ((seq1 * Ns) + (seq2 * Ns)) . n by SEQ_1:11 ; :: thesis: verum

end;

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

now

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:21
.= (seq1 . (Ns . n)) - (seq2 . (Ns . n)) by Th6
.= ((seq1 * Ns) . n) - (seq2 . (Ns . n)) by FUNCT_2:21
.= ((seq1 * Ns) . n) - ((seq2 * Ns) . n) by FUNCT_2:21
.= ((seq1 * Ns) - (seq2 * Ns)) . n by Th6 ; :: thesis: verum

end;

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

now

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:21
.= (seq1 . (Ns . n)) * (seq2 . (Ns . n)) by SEQ_1:12
.= ((seq1 * Ns) . n) * (seq2 . (Ns . n)) by FUNCT_2:21
.= ((seq1 * Ns) . n) * ((seq2 * Ns) . n) by FUNCT_2:21
.= ((seq1 * Ns) (#) (seq2 * Ns)) . n by SEQ_1:12 ; :: thesis: verum

end;

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