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

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

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

end;

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