let seq8, seq9 be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds seq8 . n = |.(seq . n).| ) & ( for n being Element of NAT holds seq9 . n = |.(seq . n).| ) implies seq8 = seq9 )
assume that
A1: for n being Element of NAT holds seq8 . n = |.(seq . n).| and
A2: for n being Element of NAT holds seq9 . n = |.(seq . n).| ; :: thesis: seq8 = seq9

now

let n be Element of NAT ; :: thesis: seq8 . n = seq9 . n
seq9 . n = |.(seq . n).| by A2;
hence seq8 . n = seq9 . n by A1; :: thesis: verum

end;

hence seq8 = seq9 by FUNCT_2:113; :: thesis: verum