let A, B be Functional_Sequence of X,Y; :: thesis: ( ( for n being Nat holds A . n = (F . n) | D ) & ( for n being Nat holds B . n = (F . n) | D ) implies A = B )
assume that
A1: for n being Nat holds A . n = (F . n) | D and
A2: for n being Nat holds B . n = (F . n) | D ; :: thesis: A = B
let x be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: A . x = B . x
thus A . x = (F . x) | D by A1
.= B . x by A2 ; :: thesis: verum