take A ; :: thesis: ( dom A = dom A & ( for j being Element of NAT st j in dom A & j <> i holds
A . j = A . j ) & A . i c= A . i )
thus ( dom A = dom A & ( for j being Element of NAT st j in dom A & j <> i holds
A . j = A . j ) & A . i c= A . i ) ; :: thesis: verum