let seq, seq1 be Complex_Sequence; :: thesis: ( seq is non-zero & seq1 is non-zero implies (seq /" seq1) " = seq1 /" seq )
assume that
A1: seq is non-zero and
A2: seq1 is non-zero ; :: thesis: (seq /" seq1) " = seq1 /" seq
A3: seq1 " is non-zero by A2, Th30;

now

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

end;

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