let seq, seq1, seq9, seq19 be Real_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 Th8
.= ((seq9 . n) * ((seq ") . n)) * ((seq19 (#) (seq1 ")) . n) by Th8
.= ((seq9 . n) * ((seq ") . n)) * ((seq19 . n) * ((seq1 ") . n)) by Th8
.= (seq9 . n) * ((seq19 . n) * (((seq ") . n) * ((seq1 ") . n)))
.= (seq9 . n) * ((seq19 . n) * (((seq ") (#) (seq1 ")) . n)) by Th8
.= ((seq9 . n) * (seq19 . n)) * (((seq ") (#) (seq1 ")) . n)
.= ((seq9 . n) * (seq19 . n)) * (((seq (#) seq1) ") . n) by Th34
.= ((seq9 (#) seq19) . n) * (((seq (#) seq1) ") . n) by Th8
.= ((seq9 (#) seq19) /" (seq (#) seq1)) . n by Th8 ; :: thesis: verum

end;

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