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

proof

let k be Nat; :: thesis: ( k in Seg (len l) implies ex y being object st S₁[k,y] )
assume k in Seg (len l) ; :: thesis: ex y being object st S₁[k,y]
( l . k in dom f implies ex y being object st S₁[k,y] ) ;
hence ex y being object 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 A

proof

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

A6: now :: thesis: ( ( l . x in dom f & s . x = f . (l . x) & f . (l . x) in QC-variables A ) or ( not l . x in dom f & s . x = l . x ) )

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

case l . x in dom f ; :: thesis: ( s . x = f . (l . x) & f . (l . x) in QC-variables A )

hence ( s . x = f . (l . x) & f . (l . x) in QC-variables A ) by A2, A3, A4, PARTFUN1:4; :: thesis: verum

end;

case not l . x in dom f ; :: thesis: s . x = l . x

hence s . x = l . x by A2, A3, A4; :: thesis: verum

end;

end;

end;

dom l = Seg (len l) by FINSEQ_1:def 3;
hence y in QC-variables A by A2, A4, A5, A6, FINSEQ_2:11; :: thesis: verum

end;

then reconsider s = s as FinSequence of QC-variables A by FINSEQ_1:def 4;
take s ; :: thesis: ( len s = len l & ( for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom f implies s . k = f . (l . k) ) & ( not l . k in dom f implies s . k = l . k ) ) ) )
thus len s = len l by A2, FINSEQ_1:def 3; :: thesis: for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom f implies s . k = f . (l . k) ) & ( not l . k in dom f implies s . k = l . k ) )
let k be Nat; :: thesis: ( 1 <= k & k <= len l implies ( ( l . k in dom f implies s . k = f . (l . k) ) & ( not l . k in dom f implies s . k = l . k ) ) )
assume ( 1 <= k & k <= len l ) ; :: thesis: ( ( l . k in dom f implies s . k = f . (l . k) ) & ( not l . k in dom f 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 f implies s . k = f . (l . k) ) & ( not l . k in dom f implies s . k = l . k ) ) by A3; :: thesis: verum