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
A10: dom F1 = dom F and
A11: for i being Nat st i in dom F1 holds
F1 . i = width (F . i) and
A12: dom F2 = dom F and
A13: for i being Nat st i in dom F2 holds
F2 . i = width (F . i) ; :: thesis: F1 = F2

now :: thesis: for x being object st x in dom F1 holds
F1 . x = F2 . x

let x be object ; :: thesis: ( x in dom F1 implies F1 . x = F2 . x )
assume A14: x in dom F1 ; :: thesis: F1 . x = F2 . x
reconsider i = x as Element of NAT by A14;
thus F1 . x = width (F . i) by A11, A14
.= F2 . x by A10, A12, A13, A14 ; :: thesis: verum

end;

hence F1 = F2 by A10, A12, FUNCT_1:2; :: thesis: verum