let seq1, seq2 be sequence of X; ( ( for n being Nat holds seq1 . n = (Cseq . n) * (seq . n) ) & ( for n being Nat holds seq2 . n = (Cseq . n) * (seq . n) ) implies seq1 = seq2 )
assume that
A2:
for n being Nat holds seq1 . n = (Cseq . n) * (seq . n)
and
A3:
for n being Nat holds seq2 . n = (Cseq . n) * (seq . n)
; seq1 = seq2
hence
seq1 = seq2
by FUNCT_2:63; verum