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