let A be non empty set ; :: thesis: for J being interpretation of A
for f being FinSequence of CQC-WFF
for v, w being Element of Valuations_in 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 A; :: thesis: for f being FinSequence of CQC-WFF
for v, w being Element of Valuations_in 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 ; :: thesis: for v, w being Element of Valuations_in 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 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 by Def14;
let p be Element of CQC-WFF ; :: 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:11;
then for b being set 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 by TARSKI:def 3;
then A4: v | (still_not-bound_in p) = w | (still_not-bound_in p) by A1, RELAT_1:188;
J,v |= p by A2, A3, Def11;
hence J,w |= p by A4, SUBLEMMA:70; :: thesis: verum