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
A9: 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
A10: 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
A11: for z being set holds
( z in X1 iff ( z in the carrier' of G & the Source of G . z = x ) ) and
A12: n1 = card X1 by A9;
consider X2 being finite set such that
A13: for z being set holds
( z in X2 iff ( z in the carrier' of G & the Source of G . z = x ) ) and
A14: n2 = card X2 by A10;
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 Source of G . z = x ) ) by A11;
hence ( z in X1 iff z in X2 ) by A13; :: thesis: verum
end;
hence n1 = n2 by A12, A14, TARSKI:2; :: thesis: verum