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
A15: 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
A16: 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
A17: for z being set holds
( z in X1 iff ( z in the carrier' of G & the Source of G . z = x ) ) and
A18: n1 = card X1 by A15;
consider X2 being finite set such that
A19: for z being set holds
( z in X2 iff ( z in the carrier' of G & the Source of G . z = x ) ) and
A20: n2 = card X2 by A16;
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 A17;
hence ( z in X1 iff z in X2 ) by A19; :: thesis: verum

end;

hence n1 = n2 by A18, A20, TARSKI:2; :: thesis: verum