set U = the IfWhileAlgebra;

set I = the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra;

set A = ProgramAlgStr(# the carrier of the IfWhileAlgebra, the charact of the IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra #);

( ProgramAlgStr(# the carrier of the IfWhileAlgebra, the charact of the IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra #) is partial & ProgramAlgStr(# the carrier of the IfWhileAlgebra, the charact of the IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra #) is quasi_total & ProgramAlgStr(# the carrier of the IfWhileAlgebra, the charact of the IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra #) is non-empty ) ;

then reconsider A = ProgramAlgStr(# 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 partial quasi_total non-empty strict ProgramAlgStr over J,T,X ;

take A ; :: thesis: ( A is with_empty-instruction & A is with_catenation & A is with_if-instruction & A is with_while-instruction )

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 )

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 )

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

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: verum

thus verum ; :: thesis: verum

set I = the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra;

set A = ProgramAlgStr(# the carrier of the IfWhileAlgebra, the charact of the IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra #);

( ProgramAlgStr(# the carrier of the IfWhileAlgebra, the charact of the IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra #) is partial & ProgramAlgStr(# the carrier of the IfWhileAlgebra, the charact of the IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra #) is quasi_total & ProgramAlgStr(# the carrier of the IfWhileAlgebra, the charact of the IfWhileAlgebra, the Function of (Union [|X, the Sorts of T|]), the carrier of the IfWhileAlgebra #) is non-empty ) ;

then reconsider A = ProgramAlgStr(# 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 partial quasi_total non-empty strict ProgramAlgStr over J,T,X ;

take A ; :: thesis: ( A is with_empty-instruction & A is with_catenation & A is with_if-instruction & A is with_while-instruction )

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 )

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 )

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

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: verum

thus verum ; :: thesis: verum