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

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