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

proof

let p be Element of QC-WFF ; :: 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 Th32
.= 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 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 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 Th34
.= (Fixed p) \/ (Fixed q) by A4, QC_LANG3:67
.= Fixed (p '&' q) by QC_LANG3:67 ; :: thesis: verum

end;

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

now

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

proof

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

end;

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

now

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

end;

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

end;

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

end;

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

now

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 Th38
.= Fixed p by A15, QC_LANG3:68
.= Fixed (All (y,p)) by QC_LANG3:68 ;
:: thesis: verum

end;

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

end;

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