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 ) );
A2: 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] ) & ( not 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
A3: dom s = Seg (len l) and
A4: for k being Nat st k in Seg (len l) holds
S₁[k,s . k] from FINSEQ_1:sch 1(A2);
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
A5: x in dom s and
A6: s . x = y by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A5;

now

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

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

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

end;

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

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

end;

end;

end;

hence y in QC-variables by A6; :: 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 A3, 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:27;
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 A4; :: thesis: verum

end;