let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) holds

( J,v |= p . (x,y) iff ex a being Element of A st

( v . y = a & J,v . (x | a) |= p ) )

let p be Element of CQC-WFF Al; :: thesis: for x, y being bound_QC-variable of Al

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,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 of Al; :: thesis: for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,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 Al,A

for v being Element of Valuations_in (Al,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 Al,A; :: thesis: for v being Element of Valuations_in (Al,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 (Al,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:89;

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 1;

then Val_S (v,[p,(Sbst (x,y))]) = v * (@ (Sbst (x,y))) ;

then A3: Val_S (v,[p,(Sbst (x,y))]) = v * (x .--> y) by SUBSTUT1:def 2;

y in bound_QC-variables Al ;

then y in dom v by SUBLEMMA:58;

then Val_S (v,[p,(Sbst (x,y))]) = x .--> (v . y) by A3, FUNCOP_1:17;

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 1; :: thesis: verum

for x, y being bound_QC-variable of Al

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) holds

( J,v |= p . (x,y) iff ex a being Element of A st

( v . y = a & J,v . (x | a) |= p ) )

let p be Element of CQC-WFF Al; :: thesis: for x, y being bound_QC-variable of Al

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,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 of Al; :: thesis: for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,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 Al,A

for v being Element of Valuations_in (Al,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 Al,A; :: thesis: for v being Element of Valuations_in (Al,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 (Al,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:89;

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 1;

then Val_S (v,[p,(Sbst (x,y))]) = v * (@ (Sbst (x,y))) ;

then A3: Val_S (v,[p,(Sbst (x,y))]) = v * (x .--> y) by SUBSTUT1:def 2;

y in bound_QC-variables Al ;

then y in dom v by SUBLEMMA:58;

then Val_S (v,[p,(Sbst (x,y))]) = x .--> (v . y) by A3, FUNCOP_1:17;

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 1; :: thesis: verum