consider c being non empty homogeneous quasi_total binary associative unital PartFunc of ({{} } * ),{{} };
consider a being Element of {{} };
consider x being set such that
A1: x is_a_unity_wrt c by Def3;
arity c = 2 by COMPUT_1:def 26;
then A2: dom c = 2 -tuples_on {{} } by COMPUT_1:25;
then <*a,a*> in dom c by FINSEQ_2:157;
then <*a,x*> in dom c by A1, Def1;
then reconsider x = x as Element of {{} } by A2, FINSEQ_2:158;
consider i being non empty homogeneous quasi_total ternary PartFunc of ({{} } * ),{{} };
consider w being non empty homogeneous quasi_total binary PartFunc of ({{} } * ),{{} };
ex S being strict non-empty UAStr st
( the carrier of S = {{} } & the charact of S = <*((0 -tuples_on {{} }) --> x),c*> ^ <*i,w*> & S is with_empty-instruction & S is with_catenation & S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial ) by A1, Th41;
hence ex b₁ being strict partial quasi_total non-empty UAStr st
( b₁ is with_empty-instruction & b₁ is with_catenation & b₁ is with_if-instruction & b₁ is with_while-instruction & b₁ is unital & b₁ is associative ) ; :: thesis: verum