:: More on Products of Many Sorted Algebras
:: by Mariusz Giero
::
:: Received April 29, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem Th1: :: PRALG_3:1
theorem Th2: :: PRALG_3:2
theorem Th3: :: PRALG_3:3
Lm1:
for f being Function
for x being set st x in product f holds
x is Function
;
theorem :: PRALG_3:4
canceled;
theorem :: PRALG_3:5
:: deftheorem defines const PRALG_3:def 1 :
theorem Th6: :: PRALG_3:6
theorem :: PRALG_3:7
theorem Th8: :: PRALG_3:8
theorem Th9: :: PRALG_3:9
theorem Th10: :: PRALG_3:10
theorem :: PRALG_3:11
theorem Th12: :: PRALG_3:12
theorem Th13: :: PRALG_3:13
theorem Th14: :: PRALG_3:14
theorem Th15: :: PRALG_3:15
theorem Th16: :: PRALG_3:16
theorem Th17: :: PRALG_3:17
theorem Th18: :: PRALG_3:18
theorem Th19: :: PRALG_3:19
theorem Th20: :: PRALG_3:20
theorem Th21: :: PRALG_3:21
theorem Th22: :: PRALG_3:22
theorem Th23: :: PRALG_3:23
:: deftheorem Def2 defines proj PRALG_3:def 2 :
definition
let I be non
empty set ;
let S be non
empty non
void ManySortedSign ;
let A be
MSAlgebra-Family of
I,
S;
let i be
Element of
I;
func proj A,
i -> ManySortedFunction of
(product A),
(A . i) means :
Def3:
:: PRALG_3:def 3
for
s being
Element of
S holds
it . s = proj (Carrier A,s),
i;
existence
ex b1 being ManySortedFunction of (product A),(A . i) st
for s being Element of S holds b1 . s = proj (Carrier A,s),i
uniqueness
for b1, b2 being ManySortedFunction of (product A),(A . i) st ( for s being Element of S holds b1 . s = proj (Carrier A,s),i ) & ( for s being Element of S holds b2 . s = proj (Carrier A,s),i ) holds
b1 = b2
end;
:: deftheorem Def3 defines proj PRALG_3:def 3 :
theorem Th24: :: PRALG_3:24
theorem :: PRALG_3:25
theorem Th26: :: PRALG_3:26
theorem Th27: :: PRALG_3:27
theorem Th28: :: PRALG_3:28
theorem Th29: :: PRALG_3:29
theorem :: PRALG_3:30
:: deftheorem Def4 defines MSAlgebra-Class PRALG_3:def 4 :
:: deftheorem Def5 defines / PRALG_3:def 5 :
:: deftheorem Def6 defines product PRALG_3:def 6 :
theorem :: PRALG_3:31