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 | = w | & 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 | = w | & 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 | = w | & 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 | = w | & J,v |= f holds
J,w |= f

let v, w be Element of Valuations_in (Al,A); :: thesis: ( v | = w | & J,v |= f implies J,w |= f )
assume A1: v | = w | ; :: 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 ;
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 | = w | by ;
J,v |= p by A2, A3;
hence J,w |= p by ; :: thesis: verum