let F1, F2 be FinSequence of NAT ; :: thesis: ( dom F1 = dom F & ( for i being Nat st i in dom F1 holds
F1 . i = width (F . i) ) & dom F2 = dom F & ( for i being Nat st i in dom F2 holds
F2 . i = width (F . i) ) implies F1 = F2 )
assume that
A8: ( dom F1 = dom F & ( for i being Nat st i in dom F1 holds
F1 . i = width (F . i) ) ) and
A9: ( dom F2 = dom F & ( for i being Nat st i in dom F2 holds
F2 . i = width (F . i) ) ) ; :: thesis: F1 = F2

now

let x be set ; :: thesis: ( x in dom F1 implies F1 . x = F2 . x )
assume A10: x in dom F1 ; :: thesis: F1 . x = F2 . x
reconsider i = x as Element of NAT by A10;
thus F1 . x = width (F . i) by A8, A10
.= F2 . x by A9, A10, A8 ; :: thesis: verum

end;

hence F1 = F2 by A8, A9, FUNCT_1:9; :: thesis: verum