let seq, seq1, seq9, seq19 be Complex_Sequence; :: thesis: (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1)

now :: thesis: for n being Element of NAT holds ((seq9 /" seq) (#) (seq19 /" seq1)) . n = ((seq9 (#) seq19) /" (seq (#) seq1)) . n

let n be Element of NAT ; :: thesis: ((seq9 /" seq) (#) (seq19 /" seq1)) . n = ((seq9 (#) seq19) /" (seq (#) seq1)) . n
thus ((seq9 /" seq) (#) (seq19 /" seq1)) . n = ((seq9 (#) (seq ")) . n) * ((seq19 /" seq1) . n) by VALUED_1:5
.= ((seq9 . n) * ((seq ") . n)) * ((seq19 (#) (seq1 ")) . n) by VALUED_1:5
.= ((seq9 . n) * ((seq ") . n)) * ((seq19 . n) * ((seq1 ") . n)) by VALUED_1:5
.= (seq9 . n) * ((seq19 . n) * (((seq ") . n) * ((seq1 ") . n)))
.= (seq9 . n) * ((seq19 . n) * (((seq ") (#) (seq1 ")) . n)) by VALUED_1:5
.= ((seq9 . n) * (seq19 . n)) * (((seq ") (#) (seq1 ")) . n)
.= ((seq9 . n) * (seq19 . n)) * (((seq (#) seq1) ") . n) by Th29
.= ((seq9 (#) seq19) . n) * (((seq (#) seq1) ") . n) by VALUED_1:5
.= ((seq9 (#) seq19) /" (seq (#) seq1)) . n by VALUED_1:5 ; :: thesis: verum

end;

hence (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1) by FUNCT_2:63; :: thesis: verum