let Al be QC-alphabet ; :: thesis: for x being bound_QC-variable of Al

for A being non empty set

for v being Element of Valuations_in (Al,A)

for a being Element of A

for X being set st X c= bound_QC-variables Al & not x in X holds

(v . (x | a)) | X = v | X

let x be bound_QC-variable of Al; :: thesis: for A being non empty set

for v being Element of Valuations_in (Al,A)

for a being Element of A

for X being set st X c= bound_QC-variables Al & not x in X holds

(v . (x | a)) | X = v | X

let A be non empty set ; :: thesis: for v being Element of Valuations_in (Al,A)

for a being Element of A

for X being set st X c= bound_QC-variables Al & not x in X holds

(v . (x | a)) | X = v | X

let v be Element of Valuations_in (Al,A); :: thesis: for a being Element of A

for X being set st X c= bound_QC-variables Al & not x in X holds

(v . (x | a)) | X = v | X

let a be Element of A; :: thesis: for X being set st X c= bound_QC-variables Al & not x in X holds

(v . (x | a)) | X = v | X

let X be set ; :: thesis: ( X c= bound_QC-variables Al & not x in X implies (v . (x | a)) | X = v | X )

assume that

A1: X c= bound_QC-variables Al and

A2: not x in X ; :: thesis: (v . (x | a)) | X = v | X

set f2 = v | X;

set f1 = (v . (x | a)) | X;

A3: dom ((v . (x | a)) | X) = dom (v | X) by A1, SUBLEMMA:63;

for A being non empty set

for v being Element of Valuations_in (Al,A)

for a being Element of A

for X being set st X c= bound_QC-variables Al & not x in X holds

(v . (x | a)) | X = v | X

let x be bound_QC-variable of Al; :: thesis: for A being non empty set

for v being Element of Valuations_in (Al,A)

for a being Element of A

for X being set st X c= bound_QC-variables Al & not x in X holds

(v . (x | a)) | X = v | X

let A be non empty set ; :: thesis: for v being Element of Valuations_in (Al,A)

for a being Element of A

for X being set st X c= bound_QC-variables Al & not x in X holds

(v . (x | a)) | X = v | X

let v be Element of Valuations_in (Al,A); :: thesis: for a being Element of A

for X being set st X c= bound_QC-variables Al & not x in X holds

(v . (x | a)) | X = v | X

let a be Element of A; :: thesis: for X being set st X c= bound_QC-variables Al & not x in X holds

(v . (x | a)) | X = v | X

let X be set ; :: thesis: ( X c= bound_QC-variables Al & not x in X implies (v . (x | a)) | X = v | X )

assume that

A1: X c= bound_QC-variables Al and

A2: not x in X ; :: thesis: (v . (x | a)) | X = v | X

set f2 = v | X;

set f1 = (v . (x | a)) | X;

A3: dom ((v . (x | a)) | X) = dom (v | X) by A1, SUBLEMMA:63;

now :: thesis: for b being object st b in dom ((v . (x | a)) | X) holds

((v . (x | a)) | X) . b = (v | X) . b

hence
(v . (x | a)) | X = v | X
by A3, FUNCT_1:2; :: thesis: verum((v . (x | a)) | X) . b = (v | X) . b

let b be object ; :: thesis: ( b in dom ((v . (x | a)) | X) implies ((v . (x | a)) | X) . b = (v | X) . b )

assume A4: b in dom ((v . (x | a)) | X) ; :: thesis: ((v . (x | a)) | X) . b = (v | X) . b

x <> b by A2, A4;

then A5: (v . (x | a)) . b = v . b by SUBLEMMA:48;

(v . (x | a)) . b = ((v . (x | a)) | X) . b by A4, FUNCT_1:47;

hence ((v . (x | a)) | X) . b = (v | X) . b by A3, A4, A5, FUNCT_1:47; :: thesis: verum

end;assume A4: b in dom ((v . (x | a)) | X) ; :: thesis: ((v . (x | a)) | X) . b = (v | X) . b

x <> b by A2, A4;

then A5: (v . (x | a)) . b = v . b by SUBLEMMA:48;

(v . (x | a)) . b = ((v . (x | a)) | X) . b by A4, FUNCT_1:47;

hence ((v . (x | a)) | X) . b = (v | X) . b by A3, A4, A5, FUNCT_1:47; :: thesis: verum