let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for l being QC-variable_list of k holds
( P ! l is Element of CQC-WFF 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 P be QC-pred_symbol of k; :: thesis: for l being QC-variable_list of k holds
( P ! l is Element of CQC-WFF 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: ( P ! l is Element of CQC-WFF 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 ) } = {} ) )
A1: Free (P ! l) = { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in free_QC-variables ) } by QC_LANG3:54;
Fixed (P ! l) = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables ) } by QC_LANG3:64;
hence ( P ! l is Element of CQC-WFF 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 ) } = {} ) ) by A1, Th13; :: thesis: verum