let IT1, IT2 be strict SubLoop of Q; :: thesis: ( H c= [#] IT1 & ( for H2 being SubLoop of Q st H c= [#] H2 holds
[#] IT1 c= [#] H2 ) & H c= [#] IT2 & ( for H2 being SubLoop of Q st H c= [#] H2 holds
[#] IT2 c= [#] H2 ) implies IT1 = IT2 )
assume that
A12: ( H c= [#] IT1 & ( for H2 being SubLoop of Q st H c= [#] H2 holds
[#] IT1 c= [#] H2 ) ) and
A13: ( H c= [#] IT2 & ( for H2 being SubLoop of Q st H c= [#] H2 holds
[#] IT2 c= [#] H2 ) ) ; :: thesis: IT1 = IT2
A14: [#] IT1 = [#] IT2 by A12, A13;
A15: the OneF of IT1 = 1. Q by Def30
.= the OneF of IT2 by Def30 ;
the multF of IT1 = the multF of Q || the carrier of IT1 by Def30
.= the multF of IT2 by Def30, A14 ;
hence IT1 = IT2 by A14, A15; :: thesis: verum