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;
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
begin
theorem Th13:
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;
theorem
theorem
theorem Th16:
theorem
theorem
theorem Th19:
theorem
theorem
theorem Th22:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem Th33:
theorem
theorem
theorem
theorem Th37:
theorem
theorem Th39:
theorem
theorem Th41:
theorem
theorem Th43:
theorem
theorem
theorem
theorem
theorem
theorem Th49:
theorem
theorem Th51:
theorem
theorem Th53:
theorem
theorem Th55:
theorem
theorem Th57:
theorem
theorem Th59:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem