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 H2(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 H2(G) is_a_unity_wrt H2(G) by Th4;
assume the_unity_wrt H2(G) in H1(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 H2(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 )
H1(H) c= H1(G) by Th23;
then reconsider a9 = a as Element of G ;
thus e * a = (the_unity_wrt H2(G)) * a9 by Th25
.= a by A1, BINOP_1:3 ; :: thesis: a * e = a
thus a * e = a9 * (the_unity_wrt H2(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
( H2(H) . (e,a) = a & H2(H) . (a,e) = a )
let a be Element of H; :: thesis: ( H2(H) . (e,a) = a & H2(H) . (a,e) = a )
( e * a = H2(H) . (e,a) & a * e = H2(H) . (a,e) ) ;
hence ( H2(H) . (e,a) = a & H2(H) . (a,e) = a ) by A2; :: thesis: verum
end;
then e is_a_unity_wrt H2(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