let Al be QC-alphabet ; :: thesis: for l1 being FinSequence of QC-variables Al st rng l1 c= bound_QC-variables Al holds
still_not-bound_in l1 = rng l1
let l1 be FinSequence of QC-variables Al; :: thesis: ( rng l1 c= bound_QC-variables Al implies still_not-bound_in l1 = rng l1 )
A1: variables_in (l1,(bound_QC-variables Al)) = { (l1 . k) where k is Nat : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables Al ) } by QC_LANG3:def 1;
assume A2: rng l1 c= bound_QC-variables Al ; :: thesis: still_not-bound_in l1 = rng l1
A3: rng l1 c= variables_in (l1,(bound_QC-variables Al))
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng l1 or b in variables_in (l1,(bound_QC-variables Al)) )
assume A4: b in rng l1 ; :: thesis: b in variables_in (l1,(bound_QC-variables Al))
then consider k being Nat such that
A5: k in dom l1 and
A6: l1 . k = b by FINSEQ_2:10;
k in Seg (len l1) by A5, FINSEQ_1:def 3;
then ( 1 <= k & k <= len l1 ) by FINSEQ_1:1;
hence b in variables_in (l1,(bound_QC-variables Al)) by A2, A1, A4, A6; :: thesis: verum
end;
variables_in (l1,(bound_QC-variables Al)) c= rng l1
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in variables_in (l1,(bound_QC-variables Al)) or b in rng l1 )
assume b in variables_in (l1,(bound_QC-variables Al)) ; :: thesis: b in rng l1
then consider k being Nat such that
A7: b = l1 . k and
A8: ( 1 <= k & k <= len l1 ) and
l1 . k in bound_QC-variables Al by A1;
k in Seg (len l1) by A8, FINSEQ_1:1;
then k in dom l1 by FINSEQ_1:def 3;
hence b in rng l1 by A7, FUNCT_1:3; :: thesis: verum
end;
then variables_in (l1,(bound_QC-variables Al)) = rng l1 by A3;
hence still_not-bound_in l1 = rng l1 by QC_LANG3:2; :: thesis: verum