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 k being Element of NAT
for P being QC-pred_symbol of k
for l being QC-variable_list of 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 holds S₁[P ! l]
let P be QC-pred_symbol of k; :: thesis: for l being QC-variable_list of holds S₁[P ! l]
let l be QC-variable_list of ; :: thesis: S₁[P ! l]
assume A2: Free (P ! l) = {} ; :: thesis: (P ! l) . x = P ! l
A3: len (Subst l,((a. 0 ) .--> x)) = len l by Def3;

now

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

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 A4, A5;
hence contradiction by A2, QC_LANG3:66; :: thesis: verum

end;

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

end;

then Subst l,((a. 0 ) .--> x) = l by A3, FINSEQ_1:18;
hence (P ! l) . x = P ! l by Th30; :: thesis: verum

end;

A6: S₁[ VERUM ] by Th28;
A7: for p being Element of QC-WFF st S₁[p] holds
S₁[ 'not' p] by Th32, QC_LANG3:67;
A8: 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 A9: ( ( 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:69;
hence (p '&' q) . x = p '&' q by A9, Th34; :: thesis: verum

end;

A10: 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 A11: ( Free p = {} implies p . x = p ) ; :: thesis: S₁[ All y,p]
assume Free (All y,p) = {} ; :: thesis: (All y,p) . x = All y,p
then ( ( x = y implies (All y,p) . x = All y,p ) & ( x <> y implies (All y,p) . x = All y,p ) ) by A11, Th37, Th38, QC_LANG3:70;
hence (All y,p) . x = All y,p ; :: thesis: verum

end;

for p being Element of QC-WFF holds S₁[p] from QC_LANG1:sch 1(A1, A6, A7, A8, A10);
hence ( Free p = {} implies p . x = p ) ; :: thesis: verum