begin
Lm1:
for f being Function
for x being set st x in product f holds
x is Function
;
begin
begin
begin
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;
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;
begin