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
A4: dom A1 = dom X and
A5: for n being Nat st n in dom X holds
A1 . n = (MemberFunc ((X . n),A)) . x and
A6: dom A2 = dom X and
A7: 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 A8: n in dom A1 ; :: thesis: A1 . n = A2 . n
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A1 . n = (MemberFunc ((X . n),A)) . x by A4, A5, A8
.= A2 . n by A4, A7, A8 ;
hence A1 . n = A2 . n ; :: thesis: verum

end;

hence A1 = A2 by A4, A6, FINSEQ_1:13; :: thesis: verum