let k be Element of NAT ; :: thesis: for l being QC-variable_list of holds
( l is CQC-variable_list of 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 ; :: thesis: ( l is CQC-variable_list of 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 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 )

proof

assume l is CQC-variable_list of ; :: 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 ;

now

assume A1: { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } <> {} ; :: thesis: contradiction
consider x being Element of { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } ;
x in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } by A1;
then consider i being Element of NAT such that
x = l . i and
A2: ( 1 <= i & i <= len l ) and
A3: l . i in free_QC-variables ;
A4: rng l c= bound_QC-variables by RELAT_1:def 19;
i in dom l by A2, FINSEQ_3:27;
then l . i in rng l by FUNCT_1:def 5;
hence contradiction by A3, A4, QC_LANG3:42; :: 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

assume A5: { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } <> {} ; :: thesis: contradiction
consider x being Element of { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } ;
x in { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } by A5;
then consider i being Element of NAT such that
x = l . i and
A6: ( 1 <= i & i <= len l ) and
A7: l . i in fixed_QC-variables ;
A8: rng l c= bound_QC-variables by RELAT_1:def 19;
i in dom l by A6, FINSEQ_3:27;
then l . i in rng l by FUNCT_1:def 5;
hence contradiction by A7, A8, QC_LANG3:41; :: 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
A9: { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } = {} and
A10: { (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
l is bound_QC-variables -valued

proof

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

A15: 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 A12, A14;
hence contradiction by A10; :: thesis: verum

end;

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 A12, A14;
hence contradiction by A9; :: thesis: verum

end;

hence x in bound_QC-variables by A12, A13, A15, Th7; :: thesis: verum

end;

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