let seq1, seq2 be sequence of X; :: thesis: ( ( for n being Nat holds seq1 . n = (Rseq . n) * (seq . n) ) & ( for n being Nat holds seq2 . n = (Rseq . n) * (seq . n) ) implies seq1 = seq2 )
assume that
A2: for n being Nat holds seq1 . n = (Rseq . n) * (seq . n) and
A3: for n being Nat holds seq2 . n = (Rseq . n) * (seq . n) ; :: thesis: seq1 = seq2
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: K64(seq1,n) = K64(seq2,n)
seq1 . n = (Rseq . n) * (seq . n) by A2;
hence seq1 . n = seq2 . n by A3; :: thesis: verum