[mizar] definitions for incomparable (?) types

[Jesse Alama <alama@stanford.edu>]

I recently came across the definition of the attribute left_unital for
non-empty multLoopStr's.  The definition is in VECTSP_1:

definition let IT be non empty multLoopStr;
 attr IT is left_unital means
 for x being Element of IT holds 1.IT * x = x;
end;

When I browse the semantic HTML presentation of the MML the link from
the "1." in the formula above goes to the definition in GROUP_1: 

definition let G be non empty HGrStr such that A1: G is unital;
 func 1.G -> Element of G means
  for h being Element of G holds h * it = h & it * h = h;
 existence;
 uniqueness;
end;

The functor "1." requires its argument to be a unital HGrStr.  But it
doesn't look like the type "non empty multLoopStr" widens to the type
"unital HGrStr".  (I'm not sure if I'm using the term "type" and
"widen" correctly here; please let me know if I should express myself
differently.)  Thus, I'm not sure how the definition of the attribute
left_unital makes sense.  What's going on here?  I'm thoroughly
confused; any clarification would be appreciated!

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*476: Too many default signature files