let Al be QC-alphabet ; :: thesis: for k being Nat
for A being non empty set
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (P ! ll) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= P ! ll iff J,v . ((vS +* vS1) +* vS2) |= P ! ll )
let k be Nat; :: thesis: for A being non empty set
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (P ! ll) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= P ! ll iff J,v . ((vS +* vS1) +* vS2) |= P ! ll )
let A be non empty set ; :: thesis: for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (P ! ll) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= P ! ll iff J,v . ((vS +* vS1) +* vS2) |= P ! ll )
let J be interpretation of Al,A; :: thesis: for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (P ! ll) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= P ! ll iff J,v . ((vS +* vS1) +* vS2) |= P ! ll )
let P be QC-pred_symbol of k,Al; :: thesis: for ll being CQC-variable_list of k,Al
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (P ! ll) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= P ! ll iff J,v . ((vS +* vS1) +* vS2) |= P ! ll )
let ll be CQC-variable_list of k,Al; :: thesis: for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (P ! ll) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= P ! ll iff J,v . ((vS +* vS1) +* vS2) |= P ! ll )
let v be Element of Valuations_in (Al,A); :: thesis: for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (P ! ll) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= P ! ll iff J,v . ((vS +* vS1) +* vS2) |= P ! ll )
let vS, vS1, vS2 be Val_Sub of A,Al; :: thesis: ( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (P ! ll) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 implies ( J,v . vS |= P ! ll iff J,v . ((vS +* vS1) +* vS2) |= P ! ll ) )
assume that
A1: for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (P ! ll) and
A2: ( ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 ) ; :: thesis: ( J,v . vS |= P ! ll iff J,v . ((vS +* vS1) +* vS2) |= P ! ll )
A3: for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in ll

proof

let y be bound_QC-variable of Al; :: thesis: ( y in dom vS1 implies not y in still_not-bound_in ll )
assume y in dom vS1 ; :: thesis: not y in still_not-bound_in ll
then not y in still_not-bound_in (P ! ll) by A1;
hence not y in still_not-bound_in ll by QC_LANG3:5; :: thesis: verum

end;

A4: ( (v . ((vS +* vS1) +* vS2)) *' ll in J . P iff (Valid ((P ! ll),J)) . (v . ((vS +* vS1) +* vS2)) = TRUE ) by VALUAT_1:7;
( (Valid ((P ! ll),J)) . (v . vS) = TRUE iff (v . vS) *' ll in J . P ) by VALUAT_1:7;
hence ( J,v . vS |= P ! ll iff J,v . ((vS +* vS1) +* vS2) |= P ! ll ) by A2, A3, A4, Th74, VALUAT_1:def 7; :: thesis: verum