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