begin
theorem Th1:
theorem Th2:
theorem Th3:
Lm1:
for f being Function
for x being set st x in product f holds
x is Function
;
theorem
canceled;
theorem
begin
:: deftheorem defines const PRALG_3:def 1 :
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
begin
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
begin
definition
let I be non
empty set ;
let S be non
empty non
void ManySortedSign ;
canceled;let A be
MSAlgebra-Family of
I,
S;
let i be
Element of
I;
func proj A,
i -> ManySortedFunction of ,
(product A) means :
Def3:
for
s being
Element of holds
it . s = proj (Carrier A,s),
i;
existence
ex b1 being ManySortedFunction of ,(product A) st
for s being Element of holds b1 . s = proj (Carrier A,s),i
uniqueness
for b1, b2 being ManySortedFunction of ,(product A) st ( for s being Element of holds b1 . s = proj (Carrier A,s),i ) & ( for s being Element of holds b2 . s = proj (Carrier A,s),i ) holds
b1 = b2
end;
:: deftheorem PRALG_3:def 2 :
canceled;
:: deftheorem Def3 defines proj PRALG_3:def 3 :
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem
begin
:: 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