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