begin
Lm1:
[#] REAL = dom (AffineMap ((1 / 2),0))
by FUNCT_2:def 1;
Lm2:
[#] REAL = dom (sin * (AffineMap (2,0)))
by FUNCT_2:def 1;
Lm3:
dom ((1 / 4) (#) (sin * (AffineMap (2,0)))) = [#] REAL
by FUNCT_2:def 1;
begin
Lm4:
dom (AffineMap (2,0)) = [#] REAL
by FUNCT_2:def 1;
Lm5:
dom ((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) = REAL
by FUNCT_2:def 1;
begin