let K be non empty doubleLoopStr ; :: thesis: ( ( for x, y being Scalar of K holds (id K) . (x * y) = ((id K) . x) * ((id K) . y) ) & (id K) . (1_ K) = 1_ K )
set J = id K;
thus for x, y being Scalar of K holds (id K) . (x * y) = ((id K) . x) * ((id K) . y) :: thesis: (id K) . (1_ K) = 1_ K

proof

let x, y be Scalar of K; :: thesis: (id K) . (x * y) = ((id K) . x) * ((id K) . y)
( (id K) . (x * y) = x * y & (id K) . x = x ) by FUNCT_1:18;
hence (id K) . (x * y) = ((id K) . x) * ((id K) . y) by FUNCT_1:18; :: thesis: verum

end;

thus (id K) . (1_ K) = 1_ K by FUNCT_1:18; :: thesis: verum