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

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

hence
a1 = a2
by FUNCT_2:12; :: thesis: verum
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;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