:: Extensions of Mappings on Generator Set
:: by Artur Korni{\l}owicz
::
:: Received March 23, 1995
:: Copyright (c) 1995 Association of Mizar Users
Lm1:
for I being set
for A, B, C being ManySortedSet of
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedSet of
theorem :: EXTENS_1:1
canceled;
theorem :: EXTENS_1:2
canceled;
theorem :: EXTENS_1:3
canceled;
theorem :: EXTENS_1:4
canceled;
theorem :: EXTENS_1:5
theorem :: EXTENS_1:6
theorem :: EXTENS_1:7
theorem Th8: :: EXTENS_1:8
theorem :: EXTENS_1:9
theorem :: EXTENS_1:10
theorem :: EXTENS_1:11
theorem :: EXTENS_1:12
theorem :: EXTENS_1:13
theorem :: EXTENS_1:14
theorem :: EXTENS_1:15
theorem Th16: :: EXTENS_1:16
theorem Th17: :: EXTENS_1:17
theorem Th18: :: EXTENS_1:18
theorem :: EXTENS_1:19
theorem :: EXTENS_1:20
theorem :: EXTENS_1:21
theorem :: EXTENS_1:22
theorem :: EXTENS_1:23