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

proof

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

end;

A11: dom (vS1 | ((dom vS1) \ {x})) misses {x} by A7, XBOOLE_1:63, XBOOLE_1:79;
A12: 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: (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v . ((vS +* vS1) +* vS2)) . (x | a)
dom (vS1 | ((dom vS1) \ {x})) misses dom (x | a) by A11, Th59;
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 A13: (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 A6, Th59;
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 A13, FUNCT_4:35;
then A14: (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;

A15: now

assume x in dom vS1 ; :: thesis: (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* ((vS1 +* vS2) +* (x | a))
then A16: (vS1 | ((dom vS1) \ {x})) +* (x .--> (vS1 . x)) = vS1 by Th2;

A17: now

assume not x in dom vS2 ; :: thesis: (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* ((vS1 +* vS2) +* (x | a))
then vS2 | ((dom vS2) \ {x}) = vS2 | (dom vS2) by ZFMISC_1:57;
then vS2 | ((dom vS2) \ {x}) = vS2 by RELAT_1:68;
then A18: (vS2 | ((dom vS2) \ {x})) +* {} = vS2 by FUNCT_4:21;
dom (x .--> (vS1 . x)) = {x} by FUNCOP_1:13;
then ( dom {} c= dom (x | a) & dom (x .--> (vS1 . x)) = dom (x | a) ) by Th59, XBOOLE_1:2;
hence (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* ((vS1 +* vS2) +* (x | a)) by A14, A16, A18, Th1; :: thesis: verum

end;

now

dom (x .--> (vS2 . x)) = {x} by FUNCOP_1:13;
then A19: dom (x .--> (vS2 . x)) = dom (x | a) by Th59;
dom (x .--> (vS1 . x)) = {x} by FUNCOP_1:13;
then A20: dom (x .--> (vS1 . x)) = dom (x | a) by Th59;
assume x in dom vS2 ; :: thesis: (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* ((vS1 +* vS2) +* (x | a))
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 A14, A16, A20, A19, Th1; :: thesis: verum

end;

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

end;

now

A21: dom {} c= dom (x | a) by XBOOLE_1:2;
assume not x in dom vS1 ; :: thesis: (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* ((vS1 +* vS2) +* (x | a))
then vS1 | ((dom vS1) \ {x}) = vS1 | (dom vS1) by ZFMISC_1:57;
then A22: vS1 | ((dom vS1) \ {x}) = vS1 by RELAT_1:68;
then A23: (vS1 | ((dom vS1) \ {x})) +* {} = vS1 by FUNCT_4:21;

A24: now

dom (x .--> (vS2 . x)) = {x} by FUNCOP_1:13;
then A25: dom (x .--> (vS2 . x)) = dom (x | a) by Th59;
assume x in dom vS2 ; :: thesis: (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* ((vS1 +* vS2) +* (x | a))
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 A14, A23, A21, A25, Th1; :: thesis: verum

end;

now

assume not x in dom vS2 ; :: thesis: (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v +* vS) +* ((vS1 +* vS2) +* (x | a))
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 A14, A22, RELAT_1:68; :: thesis: verum

end;

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

end;

then (v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = ((v +* vS) +* (vS1 +* vS2)) +* (x | a) by A15, 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: verum

end;

A26: ( ( 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 A27: for a being Element of A holds J,(v . ((vS +* vS1) +* vS2)) . (x | a) |= p ; :: thesis: for a being Element of A holds J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p
let a be Element of A; :: thesis: J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p
(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v . ((vS +* vS1) +* vS2)) . (x | a) by A12;
hence J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p by A27; :: thesis: verum

end;

A28: ( ( 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 A29: for a being Element of A holds J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p ; :: thesis: for a being Element of A holds J,(v . vS) . (x | a) |= p
let a be Element of A; :: thesis: J,(v . vS) . (x | a) |= p
dom (vS2 | ((dom vS2) \ {x})) misses dom (x | a) by A6, Th59;
then ( J,(v . vS) . (x | a) |= p iff J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p ) by A1, A8, A5;
hence J,(v . vS) . (x | a) |= p by A29; :: thesis: verum

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 A30: for a being Element of A holds J,(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) |= p ; :: thesis: for a being Element of A holds J,(v . ((vS +* vS1) +* vS2)) . (x | a) |= p
let a be Element of A; :: thesis: J,(v . ((vS +* vS1) +* vS2)) . (x | a) |= p
(v . vS) . (((x | a) +* (vS1 | ((dom vS1) \ {x}))) +* (vS2 | ((dom vS2) \ {x}))) = (v . ((vS +* vS1) +* vS2)) . (x | a) by A12;
hence J,(v . ((vS +* vS1) +* vS2)) . (x | a) |= p by A30; :: thesis: verum

end;

hence ( J,v . vS |= All (x,p) iff J,v . ((vS +* vS1) +* vS2) |= All (x,p) ) by A9, A28, A26, Th51; :: thesis: verum