let p be Element of CQC-WFF ; :: thesis: for x, y being bound_QC-variable
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A holds
( J,v |= p . x,y iff ex a being Element of A st
( v . y = a & J,v . (x | a) |= p ) )
let x, y be bound_QC-variable; :: thesis: for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A holds
( J,v |= p . x,y iff ex a being Element of A st
( v . y = a & J,v . (x | a) |= p ) )
let A be non empty set ; :: thesis: for J being interpretation of A
for v being Element of Valuations_in A holds
( J,v |= p . x,y iff ex a being Element of A st
( v . y = a & J,v . (x | a) |= p ) )
let J be interpretation of A; :: thesis: for v being Element of Valuations_in A holds
( J,v |= p . x,y iff ex a being Element of A st
( v . y = a & J,v . (x | a) |= p ) )
let v be Element of Valuations_in A; :: thesis: ( J,v |= p . x,y iff ex a being Element of A st
( v . y = a & J,v . (x | a) |= p ) )
A1: ( J,v |= CQC_Sub [p,(Sbst x,y)] iff J,v . (Val_S v,[p,(Sbst x,y)]) |= [p,(Sbst x,y)] ) by SUBLEMMA:93;
A2: ( J,v . (Val_S v,[p,(Sbst x,y)]) |= [p,(Sbst x,y)] iff J,v . (Val_S v,[p,(Sbst x,y)]) |= p ) by Th23;
Val_S v,[p,(Sbst x,y)] = v * (@ ([p,(Sbst x,y)] `2 )) by SUBLEMMA:def 2;
then Val_S v,[p,(Sbst x,y)] = v * (@ (Sbst x,y)) by MCART_1:7;
then A3: Val_S v,[p,(Sbst x,y)] = v * (x .--> y) by SUBSTUT1:def 2;
y in bound_QC-variables ;
then y in dom v by SUBLEMMA:59;
then Val_S v,[p,(Sbst x,y)] = x .--> (v . y) by A3, FUNCOP_1:23;
hence ( J,v |= p . x,y iff ex a being Element of A st
( v . y = a & J,v . (x | a) |= p ) ) by A1, A2, SUBSTUT2:def 2; :: thesis: verum