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 e' = 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

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

end;

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

now

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:11;
hence the_unity_wrt the multF of G = the_unity_wrt the multF of H by BINOP_1:def 8; :: thesis: verum