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 Source 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 Source of G . z = x ) ) ) & n2 = card X ) implies n1 = n2 )
assume that
A7: ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & n1 = card X ) and
A8: ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & n2 = card X ) ; :: thesis: n1 = n2
consider X1 being finite set such that
A9: ( ( for z being set holds
( z in X1 iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & n1 = card X1 ) by A7;
consider X2 being finite set such that
A10: ( ( for z being set holds
( z in X2 iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & n2 = card X2 ) by A8;
for z being set holds
( z in X1 iff z in X2 )

proof

let z be set ; :: thesis: ( z in X1 iff z in X2 )
( z in X1 iff ( z in the carrier' of G & the Source of G . z = x ) ) by A9;
hence ( z in X1 iff z in X2 ) by A10; :: thesis: verum

end;

hence n1 = n2 by A9, A10, TARSKI:2; :: thesis: verum