let i be Nat; :: thesis: for K being non empty associative commutative well-unital doubleLoopStr holds Product (i |-> (1_ K)) = 1_ K
let K be non empty associative commutative well-unital doubleLoopStr ; :: thesis: Product (i |-> (1_ K)) = 1_ K
the_unity_wrt the multF of K = 1_ K by Th5;
hence Product (i |-> (1_ K)) = 1_ K by SETWOP_2:25; :: thesis: verum