defpred S₁[ object , object ] means ex s being QC-symbol of A st
( s = $1 & $2 = x. s );
set X = { s where s is QC-symbol of A : x. s in rng finSub } ;
A1: { s where s is QC-symbol of A : x. s in rng finSub } c= QC-symbols A

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { s where s is QC-symbol of A : x. s in rng finSub } or a in QC-symbols A )
assume a in { s where s is QC-symbol of A : x. s in rng finSub } ; :: thesis: a in QC-symbols A
then ex s being QC-symbol of A st
( a = s & x. s in rng finSub ) ;
hence a in QC-symbols A ; :: thesis: verum

end;

A2: for a being object st a in QC-symbols A holds
ex b being object st S₁[a,b]

proof

let a be object ; :: thesis: ( a in QC-symbols A implies ex b being object st S₁[a,b] )
assume a in QC-symbols A ; :: thesis: ex b being object st S₁[a,b]
then reconsider s = a as QC-symbol of A ;
take x. s ; :: thesis: S₁[a, x. s]
take s ; :: thesis: ( s = a & x. s = x. s )
thus ( s = a & x. s = x. s ) ; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = QC-symbols A & ( for a being object st a in QC-symbols A holds
S₁[a,f . a] ) ) from CLASSES1:sch 1(A2);
A4: rng (f | { s where s is QC-symbol of A : x. s in rng finSub } ) c= rng finSub

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng (f | { s where s is QC-symbol of A : x. s in rng finSub } ) or b in rng finSub )
assume b in rng (f | { s where s is QC-symbol of A : x. s in rng finSub } ) ; :: thesis: b in rng finSub
then consider a being object such that
A5: a in dom (f | { s where s is QC-symbol of A : x. s in rng finSub } ) and
A6: b = (f | { s where s is QC-symbol of A : x. s in rng finSub } ) . a by FUNCT_1:def 3;
a in { s where s is QC-symbol of A : x. s in rng finSub } by A5, RELAT_1:57;
then A7: ex s being QC-symbol of A st
( a = s & x. s in rng finSub ) ;
( b = f . a & a in dom f ) by A5, A6, FUNCT_1:47, RELAT_1:57;
then ex s being QC-symbol of A st
( s = a & b = x. s ) by A3;
hence b in rng finSub by A7; :: thesis: verum

end;

f is one-to-one

proof

let a1, a2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a1 in proj1 f or not a2 in proj1 f or not f . a1 = f . a2 or a1 = a2 )
assume that
A8: ( a1 in dom f & a2 in dom f ) and
A9: f . a1 = f . a2 ; :: thesis: a1 = a2
( ex s being QC-symbol of A st
( s = a1 & f . a1 = x. s ) & ex t being QC-symbol of A st
( t = a2 & f . a2 = x. t ) ) by A3, A8;
hence a1 = a2 by A9, XTUPLE_0:1; :: thesis: verum

end;

then f | { s where s is QC-symbol of A : x. s in rng finSub } is one-to-one by FUNCT_1:52;
then A10: dom (f | { s where s is QC-symbol of A : x. s in rng finSub } ) is finite by A4, CARD_1:59;
reconsider X = { s where s is QC-symbol of A : x. s in rng finSub } as Subset of (QC-symbols A) by A1;
for a being object holds
( a in dom (f | X) iff ( a in X & a in dom f ) ) by RELAT_1:57;
then dom (f | X) = X /\ (QC-symbols A) by A3, XBOOLE_0:def 4;
hence { s where s is QC-symbol of A : x. s in rng finSub } is finite Subset of (QC-symbols A) by A10, XBOOLE_1:28; :: thesis: verum