let D1, D2 be Real_Sequence; :: thesis: ( ( for i being natural number holds D1 . i = diameter (S . i) ) & ( for i being natural number holds D2 . i = diameter (S . i) ) implies D1 = D2 )
assume that
A4: for i being natural number holds D1 . i = diameter (S . i) and
A5: for i being natural number holds D2 . i = diameter (S . i) ; :: thesis: D1 = D2

now

let x be Element of NAT ; :: thesis: D1 . x = D2 . x
thus D1 . x = diameter (S . x) by A4
.= D2 . x by A5 ; :: thesis: verum

end;

hence D1 = D2 by FUNCT_2:113; :: thesis: verum