reconsider N = F as Num of rng F by Def16;
take Ser ((rng F),N) ; :: thesis: for N being Num of rng F st N = F holds
Ser ((rng F),N) = Ser ((rng F),N)
thus for N being Num of rng F st N = F holds
Ser ((rng F),N) = Ser ((rng F),N) ; :: thesis: verum