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

proof

let s be set ; :: thesis: ( s in NAT implies a1 . s = a2 . s )
assume A4: s in NAT ; :: thesis: a1 . s = a2 . s
a1 . s = (abs (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:18; :: thesis: verum