let f, g be Function of the carrier of s,NAT; :: thesis: ( ( for x being type of s holds f . x = card (dom (repr_of x)) ) & ( for x being type of s holds g . x = card (dom (repr_of x)) ) implies f = g )
deffunc H₂( type of s) -> Element of omega = card (dom (repr_of $1));
assume that
A1: for x being type of s holds f . x = H₂(x) and
A2: for x being type of s holds g . x = H₂(x) ; :: thesis: f = g

now :: thesis: for c being Element of s holds f . c = g . c

let c be Element of s; :: thesis: f . c = g . c
thus f . c = H₂(c) by A1
.= g . c by A2 ; :: thesis: verum

end;

hence f = g by FUNCT_2:63; :: thesis: verum