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

proof

let p, q be Element of QC-WFF A; :: 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, Th21; :: thesis: verum

end;

A4: for k being Nat
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds S₁[P ! l]

proof

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

A6: now :: thesis: for j being Nat st 1 <= j & j <= len l holds
(Subst (l,((A a. 0) .--> x))) . j = l . j

let j be Nat; :: thesis: ( 1 <= j & j <= len l implies (Subst (l,((A a. 0) .--> x))) . j = l . j )
assume A7: ( 1 <= j & j <= len l ) ; :: thesis: (Subst (l,((A a. 0) .--> x))) . j = l . j

now :: thesis: not l . j = A a. 0

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

end;

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

end;

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

end;

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

proof

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

end;

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