let n1, n2 be Element of NAT ; :: thesis: ( ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & n1 = card X ) & ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & n2 = card X ) implies n1 = n2 )
assume that
A2: ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & n1 = card X ) and
A3: ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & n2 = card X ) ; :: thesis: n1 = n2
consider X1 being finite set such that
A4: for z being set holds
( z in X1 iff ( z in the carrier' of G & the Target of G . z = x ) ) and
A5: n1 = card X1 by A2;
consider X2 being finite set such that
A6: for z being set holds
( z in X2 iff ( z in the carrier' of G & the Target of G . z = x ) ) and
A7: n2 = card X2 by A3;
for z being object holds
( z in X1 iff z in X2 )

proof

let z be object ; :: thesis: ( z in X1 iff z in X2 )
( z in X1 iff ( z in the carrier' of G & the Target of G . z = x ) ) by A4;
hence ( z in X1 iff z in X2 ) by A6; :: thesis: verum

end;

hence n1 = n2 by A5, A7, TARSKI:2; :: thesis: verum