set W = the IfWhileAlgebra;
set I = { the program-sort of S};
set p = the program-sort of S;
set f = the formula-sort of S;
( the program-sort of S in { the formula-sort of S, the program-sort of S} & { the formula-sort of S, the program-sort of S} misses the carrier of J ) by Def16, TARSKI:def 2;
then the program-sort of S nin the carrier of J by XBOOLE_0:3;
then the program-sort of S in the carrier of S \ the carrier of J by XBOOLE_0:def 5;
then consider Q being non-empty MSAlgebra over S such that
A1: ( Q is T -extension & the Sorts of Q | { the program-sort of S} = { the program-sort of S} --> the carrier of the IfWhileAlgebra ) by Th18, ZFMISC_1:31;
set U2 = the Sorts of Q;
set C = the Charact of Q;
deffunc H₁( object , object , object ) -> set = {} ;
deffunc H₂( object ) -> object = n `1 ;
consider g being Function such that
A2: dom g = [:(Union the Sorts of Q),(Union [|Y, the Sorts of Q|]):] and
A3: for x being object st x in [:(Union the Sorts of Q),(Union [|Y, the Sorts of Q|]):] holds
g . x = H₂(x) from FUNCT_1:sch 3();
rng g c= Union the Sorts of Q

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in Union the Sorts of Q )
assume x in rng g ; :: thesis: x in Union the Sorts of Q
then consider y being object such that
A4: ( y in dom g & x = g . y ) by FUNCT_1:def 3;
consider y1, y2 being object such that
A5: ( y1 in Union the Sorts of Q & y2 in Union [|Y, the Sorts of Q|] & y = [y1,y2] ) by A2, A4, ZFMISC_1:def 2;
x = [y1,y2] `1 by A5, A2, A3, A4
.= y1 ;
hence x in Union the Sorts of Q by A5; :: thesis: verum

end;

then reconsider g = g as Function of [:(Union the Sorts of Q),(Union [|Y, the Sorts of Q|]):],(Union the Sorts of Q) by A2, FUNCT_2:2;
g is sort-preserving

proof

let j be SortSymbol of S; :: according to AOFA_L00:def 10 :: thesis: g .: [:( the Sorts of Q . j),(Union [|Y, the Sorts of Q|]):] c= the Sorts of Q . j
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g .: [:( the Sorts of Q . j),(Union [|Y, the Sorts of Q|]):] or x in the Sorts of Q . j )
assume x in g .: [:( the Sorts of Q . j),(Union [|Y, the Sorts of Q|]):] ; :: thesis: x in the Sorts of Q . j
then consider y being object such that
A6: ( y in dom g & y in [:( the Sorts of Q . j),(Union [|Y, the Sorts of Q|]):] & x = g . y ) by FUNCT_1:def 6;
consider a, b being object such that
A7: ( a in the Sorts of Q . j & b in Union [|Y, the Sorts of Q|] & y = [a,b] ) by A6, ZFMISC_1:def 2;
x = [a,b] `1 by A3, A6, A7
.= a ;
hence x in the Sorts of Q . j by A7; :: thesis: verum

end;

then reconsider g = g as sort-preserving Function of [:(Union the Sorts of Q),(Union [|Y, the Sorts of Q|]):],(Union the Sorts of Q) ;
set a = the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra;
set f = the ManySortedMSSet of the Sorts of Q, the Sorts of Q;
set eq = the Function of (Union [| the Sorts of T, the Sorts of T|]),( the Sorts of Q . the formula-sort of S);
set A = BialgebraStr(# the Sorts of Q, the Charact of Q, the ManySortedMSSet of the Sorts of Q, the Sorts of Q,g, the Function of (Union [| the Sorts of T, the Sorts of T|]),( the Sorts of Q . the formula-sort of S), the carrier of the IfWhileAlgebra, the charact of the IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra #);
reconsider A = BialgebraStr(# the Sorts of Q, the Charact of Q, the ManySortedMSSet of the Sorts of Q, the Sorts of Q,g, the Function of (Union [| the Sorts of T, the Sorts of T|]),( the Sorts of Q . the formula-sort of S), the carrier of the IfWhileAlgebra, the charact of the IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra #) as non 1s-empty strict BialgebraStr over S,Y ;
take A ; :: thesis: ( A is non-empty & A is language & A is AL-correct & A is quasi_total & A is partial & A is ua-non-empty & A is with_empty-instruction & A is with_catenation & A is with_if-instruction & A is with_while-instruction & A is T -extension )
thus the Sorts of A is non-empty ; :: according to MSUALG_1:def 3 :: thesis: ( A is language & A is AL-correct & A is quasi_total & A is partial & A is ua-non-empty & A is with_empty-instruction & A is with_catenation & A is with_if-instruction & A is with_while-instruction & A is T -extension )
thus not the Sorts of A . the formula-sort of S is empty ; :: according to AOFA_L00:def 20 :: thesis: ( A is AL-correct & A is quasi_total & A is partial & A is ua-non-empty & A is with_empty-instruction & A is with_catenation & A is with_if-instruction & A is with_while-instruction & A is T -extension )
A8: the program-sort of S in { the program-sort of S} by TARSKI:def 1;
hence the carrier of A = ({ the program-sort of S} --> the carrier of the IfWhileAlgebra) . the program-sort of S by FUNCOP_1:7
.= the Sorts of A . the program-sort of S by A1, A8, FUNCT_1:49 ;
:: according to AOFA_L00:def 38 :: thesis: ( A is quasi_total & A is partial & A is ua-non-empty & A is with_empty-instruction & A is with_catenation & A is with_if-instruction & A is with_while-instruction & A is T -extension )
thus the charact of A is quasi_total ; :: according to UNIALG_1:def 2 :: thesis: ( A is partial & A is ua-non-empty & A is with_empty-instruction & A is with_catenation & A is with_if-instruction & A is with_while-instruction & A is T -extension )
thus the charact of A is homogeneous ; :: according to UNIALG_1:def 1 :: thesis: ( A is ua-non-empty & A is with_empty-instruction & A is with_catenation & A is with_if-instruction & A is with_while-instruction & A is T -extension )
thus ( the charact of A <> {} & the charact of A is non-empty ) ; :: according to UNIALG_1:def 3 :: thesis: ( A is with_empty-instruction & A is with_catenation & A is with_if-instruction & A is with_while-instruction & A is T -extension )
thus ( 1 in dom the charact of A & the charact of A . 1 is non empty homogeneous quasi_total 0 -ary PartFunc of ( the carrier of A *), the carrier of A ) by AOFA_000:def 10; :: according to AOFA_000:def 10 :: thesis: ( A is with_catenation & A is with_if-instruction & A is with_while-instruction & A is T -extension )
thus ( 2 in dom the charact of A & the charact of A . 2 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of A *), the carrier of A ) by AOFA_000:def 11; :: according to AOFA_000:def 11 :: thesis: ( A is with_if-instruction & A is with_while-instruction & A is T -extension )
thus ( 3 in dom the charact of A & the charact of A . 3 is non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of A *), the carrier of A ) by AOFA_000:def 12; :: according to AOFA_000:def 12 :: thesis: ( A is with_while-instruction & A is T -extension )
thus ( 4 in dom the charact of A & the charact of A . 4 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of A *), the carrier of A ) by AOFA_000:def 13; :: according to AOFA_000:def 13 :: thesis: A is T -extension
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of Q, the Charact of Q #) ;
hence A is T -extension by A1, Th15; :: thesis: verum