let NORM1, NORM2 be Function of (the_set_of_RealSequences_l^ p),REAL; :: thesis: ( ( for x being object st x in the_set_of_RealSequences_l^ p holds

NORM1 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) & ( for x being object st x in the_set_of_RealSequences_l^ p holds

NORM2 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) implies NORM1 = NORM2 )

assume that

A2: for x being object st x in the_set_of_RealSequences_l^ p holds

NORM1 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) and

A3: for x being object st x in the_set_of_RealSequences_l^ p holds

NORM2 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ; :: thesis: NORM1 = NORM2

A4: for z being object st z in the_set_of_RealSequences_l^ p holds

NORM1 . z = NORM2 . z

dom NORM1 = the_set_of_RealSequences_l^ p by FUNCT_2:def 1;

hence NORM1 = NORM2 by A6, A4, FUNCT_1:2; :: thesis: verum

NORM1 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) & ( for x being object st x in the_set_of_RealSequences_l^ p holds

NORM2 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) implies NORM1 = NORM2 )

assume that

A2: for x being object st x in the_set_of_RealSequences_l^ p holds

NORM1 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) and

A3: for x being object st x in the_set_of_RealSequences_l^ p holds

NORM2 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ; :: thesis: NORM1 = NORM2

A4: for z being object st z in the_set_of_RealSequences_l^ p holds

NORM1 . z = NORM2 . z

proof

A6:
dom NORM2 = the_set_of_RealSequences_l^ p
by FUNCT_2:def 1;
let z be object ; :: thesis: ( z in the_set_of_RealSequences_l^ p implies NORM1 . z = NORM2 . z )

assume A5: z in the_set_of_RealSequences_l^ p ; :: thesis: NORM1 . z = NORM2 . z

NORM1 . z = (Sum ((seq_id z) rto_power p)) to_power (1 / p) by A2, A5;

hence NORM1 . z = NORM2 . z by A3, A5; :: thesis: verum

end;assume A5: z in the_set_of_RealSequences_l^ p ; :: thesis: NORM1 . z = NORM2 . z

NORM1 . z = (Sum ((seq_id z) rto_power p)) to_power (1 / p) by A2, A5;

hence NORM1 . z = NORM2 . z by A3, A5; :: thesis: verum

dom NORM1 = the_set_of_RealSequences_l^ p by FUNCT_2:def 1;

hence NORM1 = NORM2 by A6, A4, FUNCT_1:2; :: thesis: verum