A1: A is finite ;
deffunc H₂( expression of C) -> expression of C = C at f;
A2: { H₂(w) where w is expression of C : w in A } is finite from FRAENKEL:sch 21(A1);
A at f c= { H₂(w) where w is expression of C : w in A }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A at f or x in { H₂(w) where w is expression of C : w in A } )
assume x in A at f ; :: thesis: x in { H₂(w) where w is expression of C : w in A }
then ex a being quasi-adjective of C st
( x = a at f & a in A ) ;
hence x in { H₂(w) where w is expression of C : w in A } ; :: thesis: verum

end;

hence A at f is finite by A2; :: thesis: verum