defpred S₁[ set , set ] means ( ( l . $1 in dom Sub implies $2 = Sub . (l . $1) ) & ( not l . $1 in dom Sub implies $2 = l . $1 ) );
A1: for k being Nat st k in Seg (len l) holds
ex y being set st S₁[k,y]

proof

let k be Nat; :: thesis: ( k in Seg (len l) implies ex y being set st S₁[k,y] )
assume k in Seg (len l) ; :: thesis: ex y being set st S₁[k,y]
( l . k in dom Sub implies ex y being set st S₁[k,y] ) ;
hence ex y being set st S₁[k,y] ; :: thesis: verum

end;

consider s being FinSequence such that
A2: dom s = Seg (len l) and
A3: for k being Nat st k in Seg (len l) holds
S₁[k,s . k] from FINSEQ_1:sch 1(A1);
rng s c= QC-variables

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s or y in QC-variables )
assume y in rng s ; :: thesis: y in QC-variables
then consider x being set such that
A4: x in dom s and
A5: s . x = y by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A4;

now

per cases ( l . x in dom Sub or not l . x in dom Sub ) ;

case A6: l . x in dom Sub ; :: thesis: s . x in bound_QC-variables

then s . x = Sub . (l . x) by A2, A3, A4;
hence s . x in bound_QC-variables by A6, Th1; :: thesis: verum

end;

case A7: not l . x in dom Sub ; :: thesis: s . x in QC-variables

x in dom l by A2, A4, FINSEQ_1:def 3;
then A8: l . x in rng l by FUNCT_1:3;
s . x = l . x by A2, A3, A4, A7;
hence s . x in QC-variables by A8; :: thesis: verum

end;

end;

end;

hence y in QC-variables by A5; :: thesis: verum

end;

then reconsider s = s as FinSequence of QC-variables by FINSEQ_1:def 4;
take s ; :: thesis: ( len s = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) ) ) )
thus len s = len l by A2, FINSEQ_1:def 3; :: thesis: for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) )
thus for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) ) :: thesis: verum

proof

let k be Element of NAT ; :: thesis: ( 1 <= k & k <= len l implies ( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) ) )
assume ( 1 <= k & k <= len l ) ; :: thesis: ( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) )
then k in dom l by FINSEQ_3:25;
then k in Seg (len l) by FINSEQ_1:def 3;
hence ( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) ) by A3; :: thesis: verum

end;