let x be bound_QC-variable; :: thesis: for p being Element of QC-WFF st Free p = {} holds
p . x = p
let p be Element of QC-WFF ; :: thesis: ( Free p = {} implies p . x = p )
defpred S₁[ Element of QC-WFF ] means ( Free $1 = {} implies $1 . x = $1 );
A1: for p being Element of QC-WFF st S₁[p] holds
S₁[ 'not' p] by Th32, QC_LANG3:55;
A2: for p, q being Element of QC-WFF st S₁[p] & S₁[q] holds
S₁[p '&' q]

proof

let p, q be Element of QC-WFF ; :: thesis: ( S₁[p] & S₁[q] implies S₁[p '&' q] )
assume A3: ( ( Free p = {} implies p . x = p ) & ( Free q = {} implies q . x = q ) ) ; :: thesis: S₁[p '&' q]
assume Free (p '&' q) = {} ; :: thesis: (p '&' q) . x = p '&' q
then (Free p) \/ (Free q) = {} by QC_LANG3:57;
hence (p '&' q) . x = p '&' q by A3, Th34; :: thesis: verum

end;

A4: for k being Element of NAT
for P being QC-pred_symbol of k
for l being QC-variable_list of k holds S₁[P ! l]

proof

let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for l being QC-variable_list of k holds S₁[P ! l]
let P be QC-pred_symbol of k; :: thesis: for l being QC-variable_list of k holds S₁[P ! l]
let l be QC-variable_list of k; :: thesis: S₁[P ! l]
assume A5: Free (P ! l) = {} ; :: thesis: (P ! l) . x = P ! l

A6: now

let j be Nat; :: thesis: ( 1 <= j & j <= len l implies (Subst (l,((a. 0) .--> x))) . j = l . j )
assume A7: ( 1 <= j & j <= len l ) ; :: thesis: (Subst (l,((a. 0) .--> x))) . j = l . j
A8: j in NAT by ORDINAL1:def 12;

now

assume l . j = a. 0 ; :: thesis: contradiction
then a. 0 in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } by A8, A7;
hence contradiction by A5, QC_LANG3:54; :: thesis: verum

end;

hence (Subst (l,((a. 0) .--> x))) . j = l . j by A8, A7, Th11; :: thesis: verum

end;

len (Subst (l,((a. 0) .--> x))) = len l by Def3;
then Subst (l,((a. 0) .--> x)) = l by A6, FINSEQ_1:14;
hence (P ! l) . x = P ! l by Th30; :: thesis: verum

end;

A9: for y being bound_QC-variable
for p being Element of QC-WFF st S₁[p] holds
S₁[ All (y,p)]

proof

let y be bound_QC-variable; :: thesis: for p being Element of QC-WFF st S₁[p] holds
S₁[ All (y,p)]
let p be Element of QC-WFF ; :: thesis: ( S₁[p] implies S₁[ All (y,p)] )
assume A10: ( Free p = {} implies p . x = p ) ; :: thesis: S₁[ All (y,p)]
A11: ( x = y implies (All (y,p)) . x = All (y,p) ) by Th37;
assume Free (All (y,p)) = {} ; :: thesis: (All (y,p)) . x = All (y,p)
hence (All (y,p)) . x = All (y,p) by A10, A11, Th38, QC_LANG3:58; :: thesis: verum

end;

A12: S₁[ VERUM ] by Th28;
for p being Element of QC-WFF holds S₁[p] from QC_LANG1:sch 1(A4, A12, A1, A2, A9);
hence ( Free p = {} implies p . x = p ) ; :: thesis: verum