set c = the non empty homogeneous quasi_total 2 -ary associative unital PartFunc of ({{}} *),{{}};
set a = the Element of {{}};
consider x being set such that
A1: x is_a_unity_wrt the non empty homogeneous quasi_total 2 -ary associative unital PartFunc of ({{}} *),{{}} by Def3;
arity the non empty homogeneous quasi_total 2 -ary associative unital PartFunc of ({{}} *),{{}} = 2 by COMPUT_1:def 21;
then A2: dom the non empty homogeneous quasi_total 2 -ary associative unital PartFunc of ({{}} *),{{}} = 2 -tuples_on {{}} by COMPUT_1:22;
then <* the Element of {{}}, the Element of {{}}*> in dom the non empty homogeneous quasi_total 2 -ary associative unital PartFunc of ({{}} *),{{}} by FINSEQ_2:137;
then <* the Element of {{}},x*> in dom the non empty homogeneous quasi_total 2 -ary associative unital PartFunc of ({{}} *),{{}} by A1;
then reconsider x = x as Element of {{}} by A2, FINSEQ_2:138;
set i = the non empty homogeneous quasi_total 3 -ary PartFunc of ({{}} *),{{}};
set w = the non empty homogeneous quasi_total 2 -ary PartFunc of ({{}} *),{{}};
ex S being strict non-empty UAStr st
( the carrier of S = {{}} & the charact of S = <*((0 -tuples_on {{}}) --> x), the non empty homogeneous quasi_total 2 -ary associative unital PartFunc of ({{}} *),{{}}*> ^ <* the non empty homogeneous quasi_total 3 -ary PartFunc of ({{}} *),{{}}, the non empty homogeneous quasi_total 2 -ary PartFunc of ({{}} *),{{}}*> & 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