let Al be QC-alphabet ; :: thesis:
let p be Element of CQC-WFF Al; :: thesis:
let x be bound_QC-variable of Al; :: thesis:
let A be non empty set ; :: thesis:
let J be interpretation of Al,A; :: thesis:
assume A1: 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 ) & ( 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 iff J,v . ((vS +* vS1) +* vS2) |= p ) ; :: thesis:
let v be Element of Valuations_in (Al,A); :: thesis:
let vS, vS1, vS2 be Val_Sub of A,Al; :: thesis:
assume that
A2: for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,p)) and
A3: ( ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 ) ; :: thesis:
set vS19 = vS1 | ((dom vS1) \ {x});
set vS29 = vS2 | ((dom vS2) \ {x});
A4: for y being bound_QC-variable of Al st y in dom (vS2 | ((dom vS2) \ {x})) holds
(vS2 | ((dom vS2) \ {x})) . y = (v . vS) . y by A3, Th79;
A5: dom (vS2 | ((dom vS2) \ {x})) misses {x} by XBOOLE_1:63, XBOOLE_1:79;
A6: for y being bound_QC-variable of Al st y in dom (vS1 | ((dom vS1) \ {x})) holds
not y in still_not-bound_in p by A2, Th78;
A7: ( ( for a being Element of A holds J,(v . vS) . (x | a) |= p ) implies for a being Element of A holds J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p )

assume A8: for a being Element of A holds J,(v . vS) . (x | a) |= p ; :: thesis:
let a be Element of A; :: thesis:
dom (vS2 | ((dom vS2) \ {x})) misses dom (x | a) by A5;
then ( J,(v . vS) . (x | a) |= p iff J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p ) by A1, A6, A4;
hence J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p by A8; :: thesis:

end;

A9: dom (vS1 | ((dom vS1) \ {x})) misses {x} by XBOOLE_1:63, XBOOLE_1:79;
A10: for a being Element of A holds (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v . ((vS +* vS1) +* vS2)) . (x | a)

proof

let a be Element of A; :: thesis:
dom (vS1 | ((dom vS1) \ {x})) misses dom (x | a) by A9;
then (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* (((vS1 | ((dom vS1) \ {x})) +* (x | a)) +* (vS2 | ((dom vS2) \ {x}))) by FUNCT_4:35;
then A11: (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* ((vS1 | ((dom vS1) \ {x})) +* ((x | a) +* (vS2 | ((dom vS2) \ {x})))) by FUNCT_4:14;
dom (vS2 | ((dom vS2) \ {x})) misses dom (x | a) by A5;
then (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* ((vS1 | ((dom vS1) \ {x})) +* ((vS2 | ((dom vS2) \ {x})) +* (x | a))) by A11, FUNCT_4:35;
then A12: (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* (((vS1 | ((dom vS1) \ {x})) +* (vS2 | ((dom vS2) \ {x}))) +* (x | a)) by FUNCT_4:14;

A13: now :: thesis:

assume x in dom vS1 ; :: thesis:
then A14: (vS1 | ((dom vS1) \ {x})) +* (x .--> (vS1 . x)) = vS1 by Th2;

A15: now :: thesis:

assume not x in dom vS2 ; :: thesis:
then vS2 | ((dom vS2) \ {x}) = vS2 | (dom vS2) by ZFMISC_1:57;
then vS2 | ((dom vS2) \ {x}) = vS2 ;
then A16: (vS2 | ((dom vS2) \ {x})) +* {} = vS2 ;
( dom {} c= dom (x | a) & dom (x .--> (vS1 . x)) = dom (x | a) ) ;
hence (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* ((vS1 +* vS2) +* (x | a)) by A12, A14, A16, Th1; :: thesis:

end;

now :: thesis:

A17: dom (x .--> (vS2 . x)) = dom (x | a) ;
A18: dom (x .--> (vS1 . x)) = dom (x | a) ;
assume x in dom vS2 ; :: thesis:
then (vS2 | ((dom vS2) \ {x})) +* (x .--> (vS2 . x)) = vS2 by Th2;
hence (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* ((vS1 +* vS2) +* (x | a)) by A12, A14, A18, A17, Th1; :: thesis:

end;

hence (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* ((vS1 +* vS2) +* (x | a)) by A15; :: thesis:

end;

now :: thesis:

A19: dom {} c= dom (x | a) ;
assume not x in dom vS1 ; :: thesis:
then vS1 | ((dom vS1) \ {x}) = vS1 | (dom vS1) by ZFMISC_1:57;
then A20: vS1 | ((dom vS1) \ {x}) = vS1 ;
then A21: (vS1 | ((dom vS1) \ {x})) +* {} = vS1 ;

A22: now :: thesis:

A23: dom (x .--> (vS2 . x)) = dom (x | a) ;
assume x in dom vS2 ; :: thesis:
then (vS2 | ((dom vS2) \ {x})) +* (x .--> (vS2 . x)) = vS2 by Th2;
hence (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* ((vS1 +* vS2) +* (x | a)) by A12, A21, A19, A23, Th1; :: thesis:

end;

now :: thesis:

assume not x in dom vS2 ; :: thesis:
then vS2 | ((dom vS2) \ {x}) = vS2 | (dom vS2) by ZFMISC_1:57;
hence (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* ((vS1 +* vS2) +* (x | a)) by A12, A20; :: thesis:

end;

hence (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* ((vS1 +* vS2) +* (x | a)) by A22; :: thesis:

end;

then (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = ((v +* vS) +* (vS1 +* vS2)) +* (x | a) by A13, FUNCT_4:14;
then (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (((v +* vS) +* vS1) +* vS2) +* (x | a) by FUNCT_4:14;
then (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = ((v +* (vS +* vS1)) +* vS2) +* (x | a) by FUNCT_4:14;
hence (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v . ((vS +* vS1) +* vS2)) . (x | a) by FUNCT_4:14; :: thesis:

end;

A24: ( ( for a being Element of A holds J,(v . ((vS +* vS1) +* vS2)) . (x | a) |= p ) implies for a being Element of A holds J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p )

proof

assume A25: for a being Element of A holds J,(v . ((vS +* vS1) +* vS2)) . (x | a) |= p ; :: thesis:
let a be Element of A; :: thesis:
(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v . ((vS +* vS1) +* vS2)) . (x | a) by A10;
hence J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p by A25; :: thesis:

end;

A26: ( ( for a being Element of A holds J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p ) implies for a being Element of A holds J,(v . vS) . (x | a) |= p )

proof

assume A27: for a being Element of A holds J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p ; :: thesis:
let a be Element of A; :: thesis:
dom (vS2 | ((dom vS2) \ {x})) misses dom (x | a) by A5;
then ( J,(v . vS) . (x | a) |= p iff J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p ) by A1, A6, A4;
hence J,(v . vS) . (x | a) |= p by A27; :: thesis:

end;

( ( for a being Element of A holds J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p ) implies for a being Element of A holds J,(v . ((vS +* vS1) +* vS2)) . (x | a) |= p )

proof

assume A28: for a being Element of A holds J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p ; :: thesis:
let a be Element of A; :: thesis:
(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v . ((vS +* vS1) +* vS2)) . (x | a) by A10;
hence J,(v . ((vS +* vS1) +* vS2)) . (x | a) |= p by A28; :: thesis:

end;

hence ( J,v . vS |= All (x,p) iff J,v . ((vS +* vS1) +* vS2) |= All (x,p) ) by A7, A26, A24, Th50; :: thesis: