let seq', seq, seq1', seq1 be Real_Sequence; :: thesis: (seq' /" seq) (#) (seq1' /" seq1) = (seq' (#) seq1') /" (seq (#) seq1)

now

let n be Element of NAT ; :: thesis: ((seq' /" seq) (#) (seq1' /" seq1)) . n = ((seq' (#) seq1') /" (seq (#) seq1)) . n
thus ((seq' /" seq) (#) (seq1' /" seq1)) . n = ((seq' (#) (seq " )) . n) * ((seq1' /" seq1) . n) by Th12
.= ((seq' . n) * ((seq " ) . n)) * ((seq1' (#) (seq1 " )) . n) by Th12
.= ((seq' . n) * ((seq " ) . n)) * ((seq1' . n) * ((seq1 " ) . n)) by Th12
.= (seq' . n) * ((seq1' . n) * (((seq " ) . n) * ((seq1 " ) . n)))
.= (seq' . n) * ((seq1' . n) * (((seq " ) (#) (seq1 " )) . n)) by Th12
.= ((seq' . n) * (seq1' . n)) * (((seq " ) (#) (seq1 " )) . n)
.= ((seq' . n) * (seq1' . n)) * (((seq (#) seq1) " ) . n) by Th44
.= ((seq' (#) seq1') . n) * (((seq (#) seq1) " ) . n) by Th12
.= ((seq' (#) seq1') /" (seq (#) seq1)) . n by Th12 ; :: thesis: verum

end;

hence (seq' /" seq) (#) (seq1' /" seq1) = (seq' (#) seq1') /" (seq (#) seq1) by FUNCT_2:113; :: thesis: verum