let a1, a2 be Cardinal-Function; :: thesis: ( dom a1 = dom f & ( for x being object st x in dom f holds
a1 . x = card (f . x) ) & dom a2 = dom f & ( for x being object st x in dom f holds
a2 . x = card (f . x) ) implies a1 = a2 )
assume that
A4: dom a1 = dom f and
A5: for x being object st x in dom f holds
a1 . x = card (f . x) and
A6: dom a2 = dom f and
A7: for x being object st x in dom f holds
a2 . x = card (f . x) ; :: thesis: a1 = a2

now :: thesis: for x being object st x in dom f holds
a1 . x = a2 . x

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

end;

hence a1 = a2 by A4, A6; :: thesis: verum