let Al be QC-alphabet ; :: thesis: for A being non empty set

for J being interpretation of Al,A

for f being FinSequence of CQC-WFF Al

for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in f) = w | (still_not-bound_in f) & J,v |= f holds

J,w |= f

let A be non empty set ; :: thesis: for J being interpretation of Al,A

for f being FinSequence of CQC-WFF Al

for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in f) = w | (still_not-bound_in f) & J,v |= f holds

J,w |= f

let J be interpretation of Al,A; :: thesis: for f being FinSequence of CQC-WFF Al

for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in f) = w | (still_not-bound_in f) & J,v |= f holds

J,w |= f

let f be FinSequence of CQC-WFF Al; :: thesis: for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in f) = w | (still_not-bound_in f) & J,v |= f holds

J,w |= f

let v, w be Element of Valuations_in (Al,A); :: thesis: ( v | (still_not-bound_in f) = w | (still_not-bound_in f) & J,v |= f implies J,w |= f )

assume A1: v | (still_not-bound_in f) = w | (still_not-bound_in f) ; :: thesis: ( not J,v |= f or J,w |= f )

assume J,v |= f ; :: thesis: J,w |= f

then A2: J,v |= rng f ;

let p be Element of CQC-WFF Al; :: according to CALCUL_1:def 11,CALCUL_1:def 14 :: thesis: ( p in rng f implies J,w |= p )

assume A3: p in rng f ; :: thesis: J,w |= p

ex i being Nat st

( i in dom f & p = f . i ) by A3, FINSEQ_2:10;

then for b being object st b in still_not-bound_in p holds

b in still_not-bound_in f by Def5;

then still_not-bound_in p c= still_not-bound_in f ;

then A4: v | (still_not-bound_in p) = w | (still_not-bound_in p) by A1, RELAT_1:153;

J,v |= p by A2, A3;

hence J,w |= p by A4, SUBLEMMA:68; :: thesis: verum

for J being interpretation of Al,A

for f being FinSequence of CQC-WFF Al

for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in f) = w | (still_not-bound_in f) & J,v |= f holds

J,w |= f

let A be non empty set ; :: thesis: for J being interpretation of Al,A

for f being FinSequence of CQC-WFF Al

for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in f) = w | (still_not-bound_in f) & J,v |= f holds

J,w |= f

let J be interpretation of Al,A; :: thesis: for f being FinSequence of CQC-WFF Al

for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in f) = w | (still_not-bound_in f) & J,v |= f holds

J,w |= f

let f be FinSequence of CQC-WFF Al; :: thesis: for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in f) = w | (still_not-bound_in f) & J,v |= f holds

J,w |= f

let v, w be Element of Valuations_in (Al,A); :: thesis: ( v | (still_not-bound_in f) = w | (still_not-bound_in f) & J,v |= f implies J,w |= f )

assume A1: v | (still_not-bound_in f) = w | (still_not-bound_in f) ; :: thesis: ( not J,v |= f or J,w |= f )

assume J,v |= f ; :: thesis: J,w |= f

then A2: J,v |= rng f ;

let p be Element of CQC-WFF Al; :: according to CALCUL_1:def 11,CALCUL_1:def 14 :: thesis: ( p in rng f implies J,w |= p )

assume A3: p in rng f ; :: thesis: J,w |= p

ex i being Nat st

( i in dom f & p = f . i ) by A3, FINSEQ_2:10;

then for b being object st b in still_not-bound_in p holds

b in still_not-bound_in f by Def5;

then still_not-bound_in p c= still_not-bound_in f ;

then A4: v | (still_not-bound_in p) = w | (still_not-bound_in p) by A1, RELAT_1:153;

J,v |= p by A2, A3;

hence J,w |= p by A4, SUBLEMMA:68; :: thesis: verum