let A1, A2 be FinSequence of REAL ; :: thesis: ( dom A1 = dom X & ( for n being Nat st n in dom X holds
A1 . n = (MemberFunc (X . n),A) . x ) & dom A2 = dom X & ( for n being Nat st n in dom X holds
A2 . n = (MemberFunc (X . n),A) . x ) implies A1 = A2 )
assume that
A3: ( dom A1 = dom X & ( for n being Nat st n in dom X holds
A1 . n = (MemberFunc (X . n),A) . x ) ) and
A4: ( dom A2 = dom X & ( for n being Nat st n in dom X holds
A2 . n = (MemberFunc (X . n),A) . x ) ) ; :: thesis: A1 = A2
for n being Nat st n in dom A1 holds
A1 . n = A2 . n

proof

let n be Nat; :: thesis: ( n in dom A1 implies A1 . n = A2 . n )
assume A5: n in dom A1 ; :: thesis: A1 . n = A2 . n
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A1 . n = (MemberFunc (X . n),A) . x by A3, A5
.= A2 . n by A3, A4, A5 ;
hence A1 . n = A2 . n ; :: thesis: verum

end;

hence A1 = A2 by A3, A4, FINSEQ_1:17; :: thesis: verum