let a1, a2 be Real_Sequence; :: thesis: ( ( for n being Nat holds a1 . n = |.(x . n).| to_power p ) & ( for n being Nat holds a2 . n = |.(x . n).| to_power p ) implies a1 = a2 )
assume that
A2: for n being Nat holds a1 . n = |.(x . n).| to_power p and
A3: for n being Nat holds a2 . n = |.(x . n).| to_power p ; :: thesis: a1 = a2
for s being object st s in NAT holds
a1 . s = a2 . s

proof

let s be object ; :: thesis: ( s in NAT implies a1 . s = a2 . s )
assume A4: s in NAT ; :: thesis: a1 . s = a2 . s
a1 . s = |.(x . s).| to_power p by A2, A4
.= a2 . s by A3, A4 ;
hence a1 . s = a2 . s ; :: thesis: verum

end;

hence a1 = a2 by FUNCT_2:12; :: thesis: verum