let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A holds Fixed (p . x) = Fixed p
let x be bound_QC-variable of A; :: thesis: for p being Element of QC-WFF A holds Fixed (p . x) = Fixed p
let p be Element of QC-WFF A; :: thesis: Fixed (p . x) = Fixed p
defpred S₁[ Element of QC-WFF A] means Fixed ($1 . x) = Fixed $1;
A1: for p being Element of QC-WFF A st S₁[p] holds
S₁[ 'not' p]

proof

let p be Element of QC-WFF A; :: thesis: ( S₁[p] implies S₁[ 'not' p] )
assume A2: Fixed (p . x) = Fixed p ; :: thesis: S₁[ 'not' p]
thus Fixed (('not' p) . x) = Fixed ('not' (p . x)) by Th19
.= Fixed p by A2, QC_LANG3:65
.= Fixed ('not' p) by QC_LANG3:65 ; :: thesis: verum

end;

A3: 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 A4: ( Fixed (p . x) = Fixed p & Fixed (q . x) = Fixed q ) ; :: thesis: S₁[p '&' q]
thus Fixed ((p '&' q) . x) = Fixed ((p . x) '&' (q . x)) by Th21
.= (Fixed p) \/ (Fixed q) by A4, QC_LANG3:67
.= Fixed (p '&' q) by QC_LANG3:67 ; :: thesis: verum

end;

A5: 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]
set F1 = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } ;
set ll = Subst (l,((A a. 0) .--> x));
set F2 = { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ;
A6: len l = len (Subst (l,((A a. 0) .--> x))) by Def1;

now :: thesis: for y being object holds
( ( y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } implies y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ) & ( y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } implies y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } ) )

let y be object ; :: thesis: ( ( y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } implies y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ) & ( y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } implies y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } ) )
thus ( y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } implies y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ) :: thesis: ( y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } implies y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } )

proof

assume y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } ; :: thesis: y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) }
then consider i being Nat such that
A7: y = l . i and
A8: ( 1 <= i & i <= len l ) and
A9: l . i in fixed_QC-variables A ;
l . i <> A a. 0 by A9, QC_LANG3:32;
then (Subst (l,((A a. 0) .--> x))) . i = l . i by A8, Th3;
hence y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } by A6, A7, A8, A9; :: thesis: verum

end;

assume y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ; :: thesis: y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) }
then consider i being Nat such that
A10: y = (Subst (l,((A a. 0) .--> x))) . i and
A11: ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) ) and
A12: (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ;

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

assume l . i = A a. 0 ; :: thesis: contradiction
then (Subst (l,((A a. 0) .--> x))) . i = x by A6, A11, Th3;
hence contradiction by A12, Lm1; :: thesis: verum

end;

then (Subst (l,((A a. 0) .--> x))) . i = l . i by A6, A11, Th3;
hence y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } by A6, A10, A11, A12; :: thesis: verum

end;

then A13: { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } = { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } by TARSKI:2;
( Fixed (P ! l) = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } & Fixed (P ! (Subst (l,((A a. 0) .--> x)))) = { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ) by QC_LANG3:64;
hence S₁[P ! l] by A13, Th17; :: thesis: verum

end;

A14: 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 A15: Fixed (p . x) = Fixed p ; :: thesis: S₁[ All (y,p)]

now :: thesis: ( x <> y implies Fixed ((All (y,p)) . x) = Fixed (All (y,p)) )

assume x <> y ; :: thesis: Fixed ((All (y,p)) . x) = Fixed (All (y,p))
hence Fixed ((All (y,p)) . x) = Fixed (All (y,(p . x))) by Th25
.= Fixed p by A15, QC_LANG3:68
.= Fixed (All (y,p)) by QC_LANG3:68 ;
:: thesis: verum

end;

hence S₁[ All (y,p)] by Th24; :: thesis: verum

end;

A16: S₁[ VERUM A] by Th15;
for p being Element of QC-WFF A holds S₁[p] from QC_LANG1:sch 1(A5, A16, A1, A3, A14);
hence Fixed (p . x) = Fixed p ; :: thesis: verum