reconsider N = F as Num of rng F by Def16;
let S1, S2 be Function of NAT ,ExtREAL ; :: thesis: ( ( for N being Num of rng F st N = F holds
S1 = Ser (rng F),N ) & ( for N being Num of rng F st N = F holds
S2 = Ser (rng F),N ) implies S1 = S2 )
assume that
A1: for N being Num of rng F st N = F holds
S1 = Ser (rng F),N and
A2: for N being Num of rng F st N = F holds
S2 = Ser (rng F),N ; :: thesis: S1 = S2
thus S1 = Ser (rng F),N by A1
.= S2 by A2 ; :: thesis: verum