let k be Element of NAT ; :: thesis: for l being QC-variable_list of k holds
( l is CQC-variable_list of k iff ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } = {} ) )
let l be QC-variable_list of k; :: thesis: ( l is CQC-variable_list of k iff ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } = {} ) )
set FR = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } ;
set FI = { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } ;
thus ( l is CQC-variable_list of k implies ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } = {} ) ) :: thesis: ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } = {} implies l is CQC-variable_list of k )

proof

assume l is CQC-variable_list of k ; :: thesis: ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } = {} )
then reconsider l = l as CQC-variable_list of k ;

now

set x = the Element of { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } ;
assume { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } <> {} ; :: thesis: contradiction
then the Element of { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } ;
then consider i being Element of NAT such that
the Element of { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } = l . i and
A1: ( 1 <= i & i <= len l ) and
A2: l . i in free_QC-variables ;
i in dom l by A1, FINSEQ_3:25;
then ( rng l c= bound_QC-variables & l . i in rng l ) by FUNCT_1:def 3, RELAT_1:def 19;
hence contradiction by A2, QC_LANG3:34; :: thesis: verum

end;

hence { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } = {} ; :: thesis: { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } = {}

now

set x = the Element of { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } ;
assume { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } <> {} ; :: thesis: contradiction
then the Element of { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } in { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } ;
then consider i being Element of NAT such that
the Element of { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } = l . i and
A3: ( 1 <= i & i <= len l ) and
A4: l . i in fixed_QC-variables ;
i in dom l by A3, FINSEQ_3:25;
then ( rng l c= bound_QC-variables & l . i in rng l ) by FUNCT_1:def 3, RELAT_1:def 19;
hence contradiction by A4, QC_LANG3:33; :: thesis: verum

end;

hence { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } = {} ; :: thesis: verum

end;

assume that
A5: { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } = {} and
A6: { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } = {} ; :: thesis: l is CQC-variable_list of k
l is bound_QC-variables -valued

proof

let x be set ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not x in proj2 l or x in bound_QC-variables )
A7: rng l c= QC-variables by FINSEQ_1:def 4;
assume x in rng l ; :: thesis: x in bound_QC-variables
then consider i being set such that
A8: i in dom l and
A9: l . i = x by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A8;
A10: ( 1 <= i & i <= len l ) by A8, FINSEQ_3:25;

A11: now

assume x in fixed_QC-variables ; :: thesis: contradiction
then x in { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } by A9, A10;
hence contradiction by A6; :: thesis: verum

end;

A12: now

assume x in free_QC-variables ; :: thesis: contradiction
then x in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } by A9, A10;
hence contradiction by A5; :: thesis: verum

end;

l . i in rng l by A8, FUNCT_1:def 3;
hence x in bound_QC-variables by A9, A7, A11, A12, Th7; :: thesis: verum

end;

hence l is CQC-variable_list of k ; :: thesis: verum