let F1, F2 be FinSequence of NAT ; :: thesis: ( dom F1 = dom F & ( for i being Nat st i in dom F1 holds
F1 . i = len (F . i) ) & dom F2 = dom F & ( for i being Nat st i in dom F2 holds
F2 . i = len (F . i) ) implies F1 = F2 )
assume that
A3: dom F1 = dom F and
A4: for i being Nat st i in dom F1 holds
F1 . i = len (F . i) and
A5: dom F2 = dom F and
A6: for i being Nat st i in dom F2 holds
F2 . i = len (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 A7: x in dom F1 ; :: thesis: F1 . x = F2 . x
reconsider i = x as Element of NAT by A7;
thus F1 . x = len (F . i) by A4, A7
.= F2 . x by A3, A5, A6, A7 ; :: thesis: verum

end;

hence F1 = F2 by A3, A5, FUNCT_1:2; :: thesis: verum