set W = the infinite IfWhileAlgebra of the generators of G;
set f = the Function of (Union [| the generators of G, the Sorts of T|]),(ElementaryInstructions the infinite IfWhileAlgebra of the generators of G);
reconsider f = the Function of (Union [| the generators of G, the Sorts of T|]),(ElementaryInstructions the infinite IfWhileAlgebra of the generators of G) as Function of (Union [| the generators of G, the Sorts of T|]), the carrier of the infinite IfWhileAlgebra of the generators of G by FUNCT_2:7;
set A = ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G,f #);
set X = the generators of G;
set J = S;
( ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G,f #) is partial & ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G,f #) is quasi_total & ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G,f #) is non-empty & not ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G,f #) is empty ) ;
then reconsider A = ProgramAlgStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G,f #) as non empty partial quasi_total non-empty strict ProgramAlgStr over S,T, the generators of G ;
( A is with_empty-instruction & A is with_catenation & A is with_if-instruction & A is with_while-instruction ) by AOFA_000:def 10, AOFA_000:def 11, AOFA_000:def 12, AOFA_000:def 13;
then reconsider A = A as non empty partial quasi_total non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction strict ProgramAlgStr over S,T, the generators of G ;
( not A is degenerated & A is well_founded & A is ECIW-strict & A is infinite )

hereby :: according to AOFA_000:def 24 :: thesis:

let I1, I2 be Element of A; :: thesis:
reconsider J1 = I1, J2 = I2 as Element of the infinite IfWhileAlgebra of the generators of G ;
( EmptyIns A = EmptyIns the infinite IfWhileAlgebra of the generators of G & I1 \; I2 = J1 \; J2 ) ;
hence ( ( I1 <> EmptyIns A implies I1 \; I2 <> I2 ) & ( I2 <> EmptyIns A implies I1 \; I2 <> I1 ) & ( ( I1 <> EmptyIns A or I2 <> EmptyIns A ) implies I1 \; I2 <> EmptyIns A ) ) by AOFA_000:def 24; :: thesis:

end;

hereby :: thesis:

let C, I1, I2 be Element of A; :: thesis:
reconsider C1 = C, J1 = I1, J2 = I2 as Element of the infinite IfWhileAlgebra of the generators of G ;
( if-then-else (C,I1,I2) = if-then-else (C1,J1,J2) & EmptyIns the infinite IfWhileAlgebra of the generators of G = EmptyIns A ) ;
hence if-then-else (C,I1,I2) <> EmptyIns A by AOFA_000:def 24; :: thesis:

end;

hereby :: thesis:

let C, I be Element of A; :: thesis:
reconsider C1 = C, J = I as Element of the infinite IfWhileAlgebra of the generators of G ;
( EmptyIns A = EmptyIns the infinite IfWhileAlgebra of the generators of G & while (C,I) = while (C1,J) ) ;
hence while (C,I) <> EmptyIns A by AOFA_000:def 24; :: thesis:

end;

hereby :: thesis:

let I1, I2, C, J1, J2 be Element of A; :: thesis:
reconsider C1 = C, K1 = I1, K2 = I2, L1 = J1, L2 = J2 as Element of the infinite IfWhileAlgebra of the generators of G ;
( if-then-else (C,J1,J2) = if-then-else (C1,L1,L2) & I1 \; I2 = K1 \; K2 & EmptyIns the infinite IfWhileAlgebra of the generators of G = EmptyIns A ) ;
hence ( I1 = EmptyIns A or I2 = EmptyIns A or I1 \; I2 <> if-then-else (C,J1,J2) ) by AOFA_000:def 24; :: thesis:

end;

hereby :: thesis:

let I1, I2, C, J be Element of A; :: thesis:
reconsider C1 = C, K1 = I1, K2 = I2, L = J as Element of the infinite IfWhileAlgebra of the generators of G ;
( EmptyIns the infinite IfWhileAlgebra of the generators of G = EmptyIns A & I1 \; I2 = K1 \; K2 & while (C,J) = while (C1,L) ) ;
hence ( I1 <> EmptyIns A & I2 <> EmptyIns A implies I1 \; I2 <> while (C,J) ) by AOFA_000:def 24; :: thesis:

end;

hereby :: thesis:

let C1, I1, I2, C2, J be Element of A; :: thesis:
reconsider C3 = C1, K1 = I1, K2 = I2, C4 = C2, L = J as Element of the infinite IfWhileAlgebra of the generators of G ;
( while (C2,J) = while (C4,L) & if-then-else (C1,I1,I2) = if-then-else (C3,K1,K2) ) ;
hence if-then-else (C1,I1,I2) <> while (C2,J) by AOFA_000:def 24; :: thesis:

end;

thus A is well_founded :: thesis:

A1: UAStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G #) = UAStr(# the carrier of A, the charact of A #) ;
then ( ElementaryInstructions the infinite IfWhileAlgebra of the generators of G = ElementaryInstructions A & ElementaryInstructions the infinite IfWhileAlgebra of the generators of G is GeneratorSet of the infinite IfWhileAlgebra of the generators of G ) by AOFA_A00:43, AOFA_000:def 25;
hence ElementaryInstructions A is GeneratorSet of A by A1, AOFA_A00:46; :: according to AOFA_000:def 25 :: thesis:

end;

UAStr(# the carrier of A, the charact of A #) = UAStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G #) ;
then signature A = signature the infinite IfWhileAlgebra of the generators of G by AOFA_A00:47;
hence signature A = ECIW-signature by AOFA_000:def 27; :: according to AOFA_000:def 27 :: thesis:
UAStr(# the carrier of A, the charact of A #) = UAStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G #) ;
hence ElementaryInstructions A is infinite by AOFA_A00:43; :: according to AOFA_000:def 23 :: thesis:

end;

then reconsider A = A as infinite strict IfWhileAlgebra of the generators of G ;
take A ; :: thesis:
UAStr(# the carrier of A, the charact of A #) = UAStr(# the carrier of the infinite IfWhileAlgebra of the generators of G, the charact of the infinite IfWhileAlgebra of the generators of G #) ;
then ElementaryInstructions A = ElementaryInstructions the infinite IfWhileAlgebra of the generators of G by AOFA_A00:43;
hence rng the assignments of A c= ElementaryInstructions A by RELAT_1:def 19; :: according to AOFA_A01:def 13 :: thesis: