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 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]
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 ) } ;
A2: ( 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:77;
A3: 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
A4: y = l . i and
A5: ( 1 <= i & i <= len l ) and
A6: l . i in fixed_QC-variables ;
l . i <> a. 0 by A6, QC_LANG3:40;
then (Subst l,((a. 0 ) .--> x)) . i = l . i by A5, 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 A3, A4, A5, A6; :: 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
A7: y = (Subst l,((a. 0 ) .--> x)) . i and
A8: ( 1 <= i & i <= len (Subst l,((a. 0 ) .--> x)) ) and
A9: (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 A3, A8, Th11;
hence contradiction by A9, Lm1; :: thesis: verum

end;

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

end;

then { (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:2;
hence S₁[P ! l] by A2, Th30; :: thesis: verum

end;

A10: S₁[ VERUM ] by Th28;
A11: 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 A12: Fixed (p . x) = Fixed p ; :: thesis: S₁[ 'not' p]
thus Fixed (('not' p) . x) = Fixed ('not' (p . x)) by Th32
.= Fixed p by A12, QC_LANG3:78
.= Fixed ('not' p) by QC_LANG3:78 ; :: thesis: verum

end;

A13: 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 A14: ( 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 A14, QC_LANG3:80
.= Fixed (p '&' q) by QC_LANG3:80 ; :: thesis: verum

end;

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

end;

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

end;

for p being Element of QC-WFF holds S₁[p] from QC_LANG1:sch 1(A1, A10, A11, A13, A15);
hence Fixed (p . x) = Fixed p ; :: thesis: verum