let G be non empty multMagma ; :: thesis: for H being non empty SubStr of G st G is unital & the_unity_wrt the multF of G in the carrier of H holds
( H is unital & the_unity_wrt the multF of G = the_unity_wrt the multF of H )
let H be non empty SubStr of G; :: thesis: ( G is unital & the_unity_wrt the multF of G in the carrier of H implies ( H is unital & the_unity_wrt the multF of G = the_unity_wrt the multF of H ) )
set e9 = the_unity_wrt H₂(G);
assume G is unital ; :: thesis: ( not the_unity_wrt the multF of G in the carrier of H or ( H is unital & the_unity_wrt the multF of G = the_unity_wrt the multF of H ) )
then A1: the_unity_wrt H₂(G) is_a_unity_wrt H₂(G) by Th4;
assume the_unity_wrt H₂(G) in H₁(H) ; :: thesis: ( H is unital & the_unity_wrt the multF of G = the_unity_wrt the multF of H )
then reconsider e = the_unity_wrt H₂(G) as Element of H ;

A2: now :: thesis: for a being Element of H holds
( e * a = a & a * e = a )

let a be Element of H; :: thesis: ( e * a = a & a * e = a )
H₁(H) c= H₁(G) by Th23;
then reconsider a9 = a as Element of G ;
thus e * a = (the_unity_wrt H₂(G)) * a9 by Th25
.= a by A1, BINOP_1:3 ; :: thesis: a * e = a
thus a * e = a9 * (the_unity_wrt H₂(G)) by Th25
.= a by A1, BINOP_1:3 ; :: thesis: verum

end;

hence H is unital ; :: thesis: the_unity_wrt the multF of G = the_unity_wrt the multF of H

now :: thesis: for a being Element of H holds
( H₂(H) . (e,a) = a & H₂(H) . (a,e) = a )

let a be Element of H; :: thesis: ( H₂(H) . (e,a) = a & H₂(H) . (a,e) = a )
( e * a = H₂(H) . (e,a) & a * e = H₂(H) . (a,e) ) ;
hence ( H₂(H) . (e,a) = a & H₂(H) . (a,e) = a ) by A2; :: thesis: verum

end;

then e is_a_unity_wrt H₂(H) by BINOP_1:3;
hence the_unity_wrt the multF of G = the_unity_wrt the multF of H by BINOP_1:def 8; :: thesis: verum