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) ) & ( for x, y being Scalar of K holds (id K) . (x * y) = ((id K) . x) * ((id K) . y) ) & (id K) . (1_ K) = 1_ K & id K is one-to-one & rng (id K) = the carrier of 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: ( ( for x, y being Scalar of K holds (id K) . (x * y) = ((id K) . x) * ((id K) . y) ) & (id K) . (1_ K) = 1_ K & id K is one-to-one & rng (id K) = the carrier of 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 & (id K) . y = y ) by FUNCT_1:35;
hence (id K) . (x + y) = ((id K) . x) + ((id K) . y) ; :: thesis: verum

end;

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 & id K is one-to-one & rng (id K) = the carrier of 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 & (id K) . y = y ) by FUNCT_1:35;
hence (id K) . (x * y) = ((id K) . x) * ((id K) . y) ; :: thesis: verum

end;

thus (id K) . (1_ K) = 1_ K by FUNCT_1:35; :: thesis: ( id K is one-to-one & rng (id K) = the carrier of K )
thus id K is one-to-one by FUNCT_1:52; :: thesis: rng (id K) = the carrier of K
thus rng (id K) = the carrier of K by RELAT_1:71; :: thesis: verum