let a1, a2 be Cardinal-Function; :: thesis: ( dom a1 = dom f & ( for x being set st x in dom f holds
a1 . x = card (f . x) ) & dom a2 = dom f & ( for x being set st x in dom f holds
a2 . x = card (f . x) ) implies a1 = a2 )
assume that
A1: dom a1 = dom f and
A2: for x being set st x in dom f holds
a1 . x = card (f . x) and
A3: dom a2 = dom f and
A4: for x being set st x in dom f holds
a2 . x = card (f . x) ; :: thesis: a1 = a2

now

let x be set ; :: thesis: ( x in dom f implies a1 . x = a2 . x )
assume A5: x in dom f ; :: thesis: a1 . x = a2 . x
then a1 . x = card (f . x) by A2;
hence a1 . x = a2 . x by A4, A5; :: thesis: verum

end;

hence a1 = a2 by A1, A3, FUNCT_1:2; :: thesis: verum