deffunc H₁( object ) -> set = card (f . $1);
consider g being Cardinal-Function such that
A1: dom g = dom f and
A2: for x being set st x in dom f holds
g . x = H₁(x) from CARD_3:sch 1();
take g ; :: thesis: ( dom g = dom f & ( for x being object st x in dom f holds
g . x = card (f . x) ) )
thus dom g = dom f by A1; :: thesis: for x being object st x in dom f holds
g . x = card (f . x)
let x be object ; :: thesis: ( x in dom f implies g . x = card (f . x) )
assume A3: x in dom f ; :: thesis: g . x = card (f . x)
reconsider x = x as set by TARSKI:1;
g . x = H₁(x) by A3, A2;
hence g . x = card (f . x) ; :: thesis: verum