let f1, f2 be Function of X,NAT; :: thesis: ( ( for x being Element of X holds f1 . x = card (x . O) ) & ( for x being Element of X holds f2 . x = card (x . O) ) implies f1 = f2 )
assume that
A3: for x being Element of X holds f1 . x = card (x . O) and
A4: for x being Element of X holds f2 . x = card (x . O) ; :: thesis: f1 = f2
A5: ( dom f1 = X & dom f2 = X ) by FUNCT_2:def 1;

now :: thesis: for x being object st x in X holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in X implies f1 . x = f2 . x )
assume x in X ; :: thesis: f1 . x = f2 . x
then reconsider y = x as Element of X ;
thus f1 . x = card (y . O) by A3
.= f2 . x by A4 ; :: thesis: verum

end;

hence f1 = f2 by A5; :: thesis: verum