let G be non empty doubleLoopStr ; :: thesis: id G is linear
set f = id G;
thus id G is additive ; :: according to RINGCAT1:def 1 :: thesis: ( id G is multiplicative & id G is unity-preserving )
thus id G is multiplicative :: thesis: id G is unity-preserving
proof
let x, y be Scalar of G; :: according to GROUP_6:def 6 :: thesis: (id G) . (x * y) = ((id G) . x) * ((id G) . y)
( (id G) . (x * y) = x * y & (id G) . x = x ) by FUNCT_1:18;
hence (id G) . (x * y) = ((id G) . x) * ((id G) . y) by FUNCT_1:18; :: thesis: verum
end;
thus (id G) . (1_ G) = 1_ G by FUNCT_1:18; :: according to GROUP_1:def 13 :: thesis: verum