let l1 be FinSequence of QC-variables ; :: thesis: ( rng l1 c= bound_QC-variables implies still_not-bound_in l1 = rng l1 )
assume A1: rng l1 c= bound_QC-variables ; :: thesis: still_not-bound_in l1 = rng l1
A2: variables_in l1,bound_QC-variables = { (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables ) } by QC_LANG3:def 2;
variables_in l1,bound_QC-variables = rng l1

proof

thus variables_in l1,bound_QC-variables c= rng l1 :: according to XBOOLE_0:def 10 :: thesis: rng l1 c= variables_in l1,bound_QC-variables

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in variables_in l1,bound_QC-variables or b in rng l1 )
assume b in variables_in l1,bound_QC-variables ; :: thesis: b in rng l1
then consider k being Element of NAT such that
A3: ( b = l1 . k & 1 <= k & k <= len l1 & l1 . k in bound_QC-variables ) by A2;
k in Seg (len l1) by A3, FINSEQ_1:3;
then k in dom l1 by FINSEQ_1:def 3;
hence b in rng l1 by A3, FUNCT_1:12; :: thesis: verum

end;

thus rng l1 c= variables_in l1,bound_QC-variables :: thesis: verum

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in rng l1 or b in variables_in l1,bound_QC-variables )
assume A4: b in rng l1 ; :: thesis: b in variables_in l1,bound_QC-variables
then consider k being Nat such that
A5: ( k in dom l1 & l1 . k = b ) by FINSEQ_2:11;
k in Seg (len l1) by A5, FINSEQ_1:def 3;
then ( 1 <= k & k <= len l1 ) by FINSEQ_1:3;
hence b in variables_in l1,bound_QC-variables by A1, A2, A4, A5; :: thesis: verum

end;

end;

hence still_not-bound_in l1 = rng l1 by QC_LANG3:6; :: thesis: verum