let n be natural non empty number ; :: thesis: for J being non empty non void Signature

for T being non-empty VarMSAlgebra over J

for X being V2() GeneratorSet of T

for S being non empty non void b_{1} -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X

for L being non empty IfWhileAlgebra of X,S

for A, V being Formula of L

for H being AL-theory of V,L

for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let J be non empty non void Signature; :: thesis: for T being non-empty VarMSAlgebra over J

for X being V2() GeneratorSet of T

for S being non empty non void J -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X

for L being non empty IfWhileAlgebra of X,S

for A, V being Formula of L

for H being AL-theory of V,L

for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let T be non-empty VarMSAlgebra over J; :: thesis: for X being V2() GeneratorSet of T

for S being non empty non void J -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X

for L being non empty IfWhileAlgebra of X,S

for A, V being Formula of L

for H being AL-theory of V,L

for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let X be V2() GeneratorSet of T; :: thesis: for S being non empty non void J -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X

for L being non empty IfWhileAlgebra of X,S

for A, V being Formula of L

for H being AL-theory of V,L

for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let S be non empty non void J -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X; :: thesis: for L being non empty IfWhileAlgebra of X,S

for A, V being Formula of L

for H being AL-theory of V,L

for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let L be non empty IfWhileAlgebra of X,S; :: thesis: for A, V being Formula of L

for H being AL-theory of V,L

for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let A, V be Formula of L; :: thesis: for H being AL-theory of V,L

for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let H be AL-theory of V,L; :: thesis: for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let a be SortSymbol of J; :: thesis: for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let x, y be Element of X . a; :: thesis: for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let x0, y0 be Element of Union (X extended_by ({}, the carrier of S)); :: thesis: ( x = x0 & y = y0 implies ((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H )

reconsider b = a as SortSymbol of S by Th8;

reconsider t = @ y as Element of the Sorts of L . b by Th16;

assume A1: ( x = x0 & y = y0 ) ; :: thesis: ((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

then A2: ((x := ((@ y),L)) * A) \iff (A / (x0,t)) in H by Def43;

A3: X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of L by Th23;

( a in the carrier of J & the carrier of J = dom X ) by PARTFUN1:def 2;

then b in dom (X | the carrier of S) by RELAT_1:57;

then (X extended_by ({}, the carrier of S)) . b = (X | the carrier of S) . b by FUNCT_4:13

.= X . b by FUNCT_1:49 ;

hence ((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H by A1, A2, A3, Th14; :: thesis: verum

for T being non-empty VarMSAlgebra over J

for X being V2() GeneratorSet of T

for S being non empty non void b

for L being non empty IfWhileAlgebra of X,S

for A, V being Formula of L

for H being AL-theory of V,L

for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let J be non empty non void Signature; :: thesis: for T being non-empty VarMSAlgebra over J

for X being V2() GeneratorSet of T

for S being non empty non void J -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X

for L being non empty IfWhileAlgebra of X,S

for A, V being Formula of L

for H being AL-theory of V,L

for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let T be non-empty VarMSAlgebra over J; :: thesis: for X being V2() GeneratorSet of T

for S being non empty non void J -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X

for L being non empty IfWhileAlgebra of X,S

for A, V being Formula of L

for H being AL-theory of V,L

for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let X be V2() GeneratorSet of T; :: thesis: for S being non empty non void J -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X

for L being non empty IfWhileAlgebra of X,S

for A, V being Formula of L

for H being AL-theory of V,L

for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let S be non empty non void J -extension n PC-correct QC-correct n AL-correct essential AlgLangSignature over Union X; :: thesis: for L being non empty IfWhileAlgebra of X,S

for A, V being Formula of L

for H being AL-theory of V,L

for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let L be non empty IfWhileAlgebra of X,S; :: thesis: for A, V being Formula of L

for H being AL-theory of V,L

for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let A, V be Formula of L; :: thesis: for H being AL-theory of V,L

for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let H be AL-theory of V,L; :: thesis: for a being SortSymbol of J

for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let a be SortSymbol of J; :: thesis: for x, y being Element of X . a

for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let x, y be Element of X . a; :: thesis: for x0, y0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 & y = y0 holds

((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

let x0, y0 be Element of Union (X extended_by ({}, the carrier of S)); :: thesis: ( x = x0 & y = y0 implies ((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H )

reconsider b = a as SortSymbol of S by Th8;

reconsider t = @ y as Element of the Sorts of L . b by Th16;

assume A1: ( x = x0 & y = y0 ) ; :: thesis: ((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H

then A2: ((x := ((@ y),L)) * A) \iff (A / (x0,t)) in H by Def43;

A3: X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of L by Th23;

( a in the carrier of J & the carrier of J = dom X ) by PARTFUN1:def 2;

then b in dom (X | the carrier of S) by RELAT_1:57;

then (X extended_by ({}, the carrier of S)) . b = (X | the carrier of S) . b by FUNCT_4:13

.= X . b by FUNCT_1:49 ;

hence ((x := ((@ y),L)) * A) \iff (A / (x0,y0)) in H by A1, A2, A3, Th14; :: thesis: verum