let p, q be XFinSequence; :: thesis: ( dom p = dom q & ( for k being Element of NAT st k in dom p holds
p . k = q . k ) implies p = q )
assume A1: ( dom p = dom q & ( for k being Element of NAT st k in dom p holds
p . k = q . k ) ) ; :: thesis: p = q
then for x being set st x in dom p holds
p . x = q . x ;
hence p = q by A1, FUNCT_1:9; :: thesis: verum