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