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 S1[ Element of QC-WFF A] means ( Free $1 = {} implies $1 . x = $1 );
A1: for p being Element of QC-WFF A st S1[p] holds
S1[ 'not' p] by Th19, QC_LANG3:55;
A2: for p, q being Element of QC-WFF A st S1[p] & S1[q] holds
S1[p '&' q]
proof
let p, q be Element of QC-WFF A; :: thesis: ( S1[p] & S1[q] implies S1[p '&' q] )
assume A3: ( ( Free p = {} implies p . x = p ) & ( Free q = {} implies q . x = q ) ) ; :: thesis: S1[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 S1[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 S1[P ! l]
let P be QC-pred_symbol of k,A; :: thesis: for l being QC-variable_list of k,A holds S1[P ! l]
let l be QC-variable_list of k,A; :: thesis: S1[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 S1[p] holds
S1[ All (y,p)]
proof
let y be bound_QC-variable of A; :: thesis: for p being Element of QC-WFF A st S1[p] holds
S1[ All (y,p)]
let p be Element of QC-WFF A; :: thesis: ( S1[p] implies S1[ All (y,p)] )
assume A9: ( Free p = {} implies p . x = p ) ; :: thesis: S1[ 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: S1[ VERUM A] by Th15;
for p being Element of QC-WFF A holds S1[p] from QC_LANG1:sch 1(A4, A11, A1, A2, A8);
 hence ( Free p = {} implies p . x = p ) ; :: thesis: verum