let K be non empty associative commutative well-unital doubleLoopStr ; :: thesis: for R being Element of 0 -tuples_on the carrier of K holds Product R = 1. K
let R be Element of 0 -tuples_on the carrier of K; :: thesis: Product R = 1. K
R = <*> the carrier of K ;
hence Product R = 1. K by Lm6; :: thesis: verum