let D be Polish-arity-function; :: thesis: ( D is C -extending implies D is B -extending )
assume D is C -extending ; :: thesis: D is B -extending
then A1: C c= D ;
B c= C by Def3;
then B c= D by A1;
hence D is B -extending ; :: thesis: verum