set M = multLoopStr(# (Funcs (A,H₃(G))),((H₁(G),H₃(G)) .: A),(A --> (the_unity_wrt H₁(G))) #);
H₁(G) is having_a_unity by MONOID_0:def 10;
then consider a being Element of G such that
A1: a is_a_unity_wrt H₁(G) ;
A2: ( 1. multLoopStr(# (Funcs (A,H₃(G))),((H₁(G),H₃(G)) .: A),(A --> (the_unity_wrt H₁(G))) #) = A --> (the_unity_wrt the multF of G) & .: (G,A) = multLoopStr(# (Funcs (A,H₃(G))),((H₁(G),H₃(G)) .: A),(A --> (the_unity_wrt H₁(G))) #) ) by Def3;
( a = the_unity_wrt H₁(G) & A --> a is_a_unity_wrt (H₁(G),H₃(G)) .: A ) by A1, Th9, BINOP_1:def 8;
hence .: (G,A) is non empty strict well-unital constituted-Functions multLoopStr by A2, MONOID_0:def 21; :: thesis: verum