:: by Mariusz Giero

::

:: Received April 29, 1996

:: Copyright (c) 1996-2019 Association of Mizar Users

registration

let I be set ;

let S be non empty non void ManySortedSign ;

let AF be MSAlgebra-Family of I,S;

coherence

product AF is non-empty by MSUALG_1:def 3;

end;
let S be non empty non void ManySortedSign ;

let AF be MSAlgebra-Family of I,S;

coherence

product AF is non-empty by MSUALG_1:def 3;

registration
end;

theorem Th2: :: PRALG_3:2

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for s being SortSymbol of S

for a being non empty Subset of I

for Aa being MSAlgebra-Family of a,S st A | a = Aa holds

Carrier (Aa,s) = (Carrier (A,s)) | a

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for s being SortSymbol of S

for a being non empty Subset of I

for Aa being MSAlgebra-Family of a,S st A | a = Aa holds

Carrier (Aa,s) = (Carrier (A,s)) | a

proof end;

theorem Th3: :: PRALG_3:3

for i being set

for I being non empty set

for EqR being Equivalence_Relation of I

for c1, c2 being Element of Class EqR st i in c1 & i in c2 holds

c1 = c2

for I being non empty set

for EqR being Equivalence_Relation of I

for c1, c2 being Element of Class EqR st i in c1 & i in c2 holds

c1 = c2

proof end;

Lm1: for f being Function

for x being set st x in product f holds

x is Function

;

theorem :: PRALG_3:4

for D being non empty set

for F being ManySortedFunction of D

for C being non empty functional with_common_domain set st C = rng F holds

for d being Element of D

for e being set st e in DOM C holds

(F . d) . e = ((commute F) . e) . d

for F being ManySortedFunction of D

for C being non empty functional with_common_domain set st C = rng F holds

for d being Element of D

for e being set st e in DOM C holds

(F . d) . e = ((commute F) . e) . d

proof end;

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let o be OperSymbol of S;

correctness

coherence

(Den (o,U0)) . {} is set ;

;

end;
let U0 be MSAlgebra over S;

let o be OperSymbol of S;

correctness

coherence

(Den (o,U0)) . {} is set ;

;

:: deftheorem defines const PRALG_3:def 1 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for o being OperSymbol of S holds const (o,U0) = (Den (o,U0)) . {};

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for o being OperSymbol of S holds const (o,U0) = (Den (o,U0)) . {};

theorem Th5: :: PRALG_3:5

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for o being OperSymbol of S st the_arity_of o = {} & Result (o,U0) <> {} holds

const (o,U0) in Result (o,U0)

for U0 being MSAlgebra over S

for o being OperSymbol of S st the_arity_of o = {} & Result (o,U0) <> {} holds

const (o,U0) in Result (o,U0)

proof end;

theorem :: PRALG_3:6

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for s being SortSymbol of S st the Sorts of U0 . s <> {} holds

Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }

for U0 being MSAlgebra over S

for s being SortSymbol of S st the Sorts of U0 . s <> {} holds

Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }

proof end;

theorem Th7: :: PRALG_3:7

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S st the_arity_of o = {} holds

(commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))))

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S st the_arity_of o = {} holds

(commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))))

proof end;

theorem Th8: :: PRALG_3:8

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S st the_arity_of o = {} holds

const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S st the_arity_of o = {} holds

const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))

proof end;

registration

let S be non empty non void ManySortedSign ;

let I be non empty set ;

let o be OperSymbol of S;

let A be MSAlgebra-Family of I,S;

coherence

( const (o,(product A)) is Relation-like & const (o,(product A)) is Function-like )

end;
let I be non empty set ;

let o be OperSymbol of S;

let A be MSAlgebra-Family of I,S;

coherence

( const (o,(product A)) is Relation-like & const (o,(product A)) is Function-like )

proof end;

theorem Th9: :: PRALG_3:9

for I being non empty set

for S being non empty non void ManySortedSign

for i being Element of I

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S st the_arity_of o = {} holds

(const (o,(product A))) . i = const (o,(A . i))

for S being non empty non void ManySortedSign

for i being Element of I

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S st the_arity_of o = {} holds

(const (o,(product A))) . i = const (o,(A . i))

proof end;

theorem :: PRALG_3:10

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) holds

f = const (o,(product A))

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) holds

f = const (o,(product A))

proof end;

theorem Th11: :: PRALG_3:11

for S being non empty non void ManySortedSign

for U1, U2 being MSAlgebra over S

for o being OperSymbol of S

for e being Element of Args (o,U1) st e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} holds

for F being ManySortedFunction of U1,U2 holds F # e = {}

for U1, U2 being MSAlgebra over S

for o being OperSymbol of S

for e being Element of Args (o,U1) st e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} holds

for F being ManySortedFunction of U1,U2 holds F # e = {}

proof end;

theorem Th12: :: PRALG_3:12

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for U1, U2 being non-empty MSAlgebra over S

for F being ManySortedFunction of U1,U2

for x being Element of Args (o,U1) holds x in product (doms (F * (the_arity_of o)))

for o being OperSymbol of S

for U1, U2 being non-empty MSAlgebra over S

for F being ManySortedFunction of U1,U2

for x being Element of Args (o,U1) holds x in product (doms (F * (the_arity_of o)))

proof end;

theorem Th13: :: PRALG_3:13

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for U1, U2 being non-empty MSAlgebra over S

for F being ManySortedFunction of U1,U2

for x being Element of Args (o,U1)

for n being set st n in dom (the_arity_of o) holds

(F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)

for o being OperSymbol of S

for U1, U2 being non-empty MSAlgebra over S

for F being ManySortedFunction of U1,U2

for x being Element of Args (o,U1)

for n being set st n in dom (the_arity_of o) holds

(F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)

proof end;

theorem Th14: :: PRALG_3:14

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for x being Element of Args (o,(product A)) holds x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ))))

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for x being Element of Args (o,(product A)) holds x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ))))

proof end;

theorem Th15: :: PRALG_3:15

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for x being Element of Args (o,(product A))

for n being set st n in dom (the_arity_of o) holds

x . n in product (Carrier (A,((the_arity_of o) /. n)))

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for x being Element of Args (o,(product A))

for n being set st n in dom (the_arity_of o) holds

x . n in product (Carrier (A,((the_arity_of o) /. n)))

proof end;

theorem Th16: :: PRALG_3:16

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for i being Element of I

for n being set st n in dom (the_arity_of o) holds

for s being SortSymbol of S st s = (the_arity_of o) . n holds

for y being Element of Args (o,(product A))

for g being Function st g = y . n holds

g . i in the Sorts of (A . i) . s

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for i being Element of I

for n being set st n in dom (the_arity_of o) holds

for s being SortSymbol of S st s = (the_arity_of o) . n holds

for y being Element of Args (o,(product A))

for g being Function st g = y . n holds

g . i in the Sorts of (A . i) . s

proof end;

theorem Th17: :: PRALG_3:17

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds

commute y in product (doms (A ?. o))

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds

commute y in product (doms (A ?. o))

proof end;

theorem Th18: :: PRALG_3:18

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds

y in dom (Commute (Frege (A ?. o)))

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds

y in dom (Commute (Frege (A ?. o)))

proof end;

theorem Th19: :: PRALG_3:19

for I being set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for x being Element of Args (o,(product A)) holds (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o)))

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for x being Element of Args (o,(product A)) holds (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o)))

proof end;

theorem Th20: :: PRALG_3:20

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for i being Element of I

for o being OperSymbol of S st the_arity_of o <> {} holds

for U1 being non-empty MSAlgebra over S

for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for i being Element of I

for o being OperSymbol of S st the_arity_of o <> {} holds

for U1 being non-empty MSAlgebra over S

for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))

proof end;

theorem Th21: :: PRALG_3:21

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for i being Element of I

for o being OperSymbol of S

for x being Element of Args (o,(product A))

for n being set st n in dom (the_arity_of o) holds

for f being Function st f = x . n holds

((commute x) . i) . n = f . i

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for i being Element of I

for o being OperSymbol of S

for x being Element of Args (o,(product A))

for n being set st n in dom (the_arity_of o) holds

for f being Function st f = x . n holds

((commute x) . i) . n = f . i

proof end;

theorem Th22: :: PRALG_3:22

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S st the_arity_of o <> {} holds

for y being Element of Args (o,(product A))

for i9 being Element of I

for g being Function st g = (Den (o,(product A))) . y holds

g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S st the_arity_of o <> {} holds

for y being Element of Args (o,(product A))

for i9 being Element of I

for g being Function st g = (Den (o,(product A))) . y holds

g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)

proof end;

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;

ex b_{1} being ManySortedFunction of (product A),(A . i) st

for s being Element of S holds b_{1} . s = proj ((Carrier (A,s)),i)

for b_{1}, b_{2} being ManySortedFunction of (product A),(A . i) st ( for s being Element of S holds b_{1} . s = proj ((Carrier (A,s)),i) ) & ( for s being Element of S holds b_{2} . s = proj ((Carrier (A,s)),i) ) holds

b_{1} = b_{2}

end;
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 :Def2: :: PRALG_3:def 2

for s being Element of S holds it . s = proj ((Carrier (A,s)),i);

existence for s being Element of S holds it . s = proj ((Carrier (A,s)),i);

ex b

for s being Element of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines proj PRALG_3:def 2 :

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for i being Element of I

for b_{5} being ManySortedFunction of (product A),(A . i) holds

( b_{5} = proj (A,i) iff for s being Element of S holds b_{5} . s = proj ((Carrier (A,s)),i) );

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for i being Element of I

for b

( b

theorem Th23: :: PRALG_3:23

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds

for i being Element of I holds (proj (A,i)) # x = (commute x) . i

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds

for i being Element of I holds (proj (A,i)) # x = (commute x) . i

proof end;

theorem :: PRALG_3:24

for I being non empty set

for S being non empty non void ManySortedSign

for i being Element of I

for A being MSAlgebra-Family of I,S holds proj (A,i) is_homomorphism product A,A . i

for S being non empty non void ManySortedSign

for i being Element of I

for A being MSAlgebra-Family of I,S holds proj (A,i) is_homomorphism product A,A . i

proof end;

theorem Th25: :: PRALG_3:25

for I being non empty set

for S being non empty non void ManySortedSign

for i being Element of I

for A being MSAlgebra-Family of I,S

for s being SortSymbol of S

for U1 being non-empty MSAlgebra over S

for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st

( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds

( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s )

for S being non empty non void ManySortedSign

for i being Element of I

for A being MSAlgebra-Family of I,S

for s being SortSymbol of S

for U1 being non-empty MSAlgebra over S

for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st

( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds

( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s )

proof end;

theorem Th26: :: PRALG_3:26

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for s being SortSymbol of S

for U1 being non-empty MSAlgebra over S

for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st

( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds

(commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))))

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for s being SortSymbol of S

for U1 being non-empty MSAlgebra over S

for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st

( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds

(commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))))

proof end;

theorem Th27: :: PRALG_3:27

for I being non empty set

for S being non empty non void ManySortedSign

for i being Element of I

for A being MSAlgebra-Family of I,S

for s being SortSymbol of S

for U1 being non-empty MSAlgebra over S

for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st

( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds

for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds

for x being set st x in the Sorts of U1 . s holds

for f being Function st f = (commute ((commute F) . s)) . x holds

f . i = (F9 . s) . x

for S being non empty non void ManySortedSign

for i being Element of I

for A being MSAlgebra-Family of I,S

for s being SortSymbol of S

for U1 being non-empty MSAlgebra over S

for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st

( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds

for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds

for x being set st x in the Sorts of U1 . s holds

for f being Function st f = (commute ((commute F) . s)) . x holds

f . i = (F9 . s) . x

proof end;

theorem Th28: :: PRALG_3:28

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for s being SortSymbol of S

for U1 being non-empty MSAlgebra over S

for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st

( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds

for x being set st x in the Sorts of U1 . s holds

(commute ((commute F) . s)) . x in product (Carrier (A,s))

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for s being SortSymbol of S

for U1 being non-empty MSAlgebra over S

for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st

( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds

for x being set st x in the Sorts of U1 . s holds

(commute ((commute F) . s)) . x in product (Carrier (A,s))

proof end;

theorem :: PRALG_3:29

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for U1 being non-empty MSAlgebra over S

for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st

( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds

ex H being ManySortedFunction of U1,(product A) st

( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for U1 being non-empty MSAlgebra over S

for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st

( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds

ex H being ManySortedFunction of U1,(product A) st

( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )

proof end;

definition

let I be non empty set ;

let J be ManySortedSet of I;

let S be non empty non void ManySortedSign ;

ex b_{1} being ManySortedSet of I st

for i being set st i in I holds

b_{1} . i is MSAlgebra-Family of J . i,S

end;
let J be ManySortedSet of I;

let S be non empty non void ManySortedSign ;

mode MSAlgebra-Class of S,J -> ManySortedSet of I means :Def3: :: PRALG_3:def 3

for i being set st i in I holds

it . i is MSAlgebra-Family of J . i,S;

existence for i being set st i in I holds

it . i is MSAlgebra-Family of J . i,S;

ex b

for i being set st i in I holds

b

proof end;

:: deftheorem Def3 defines MSAlgebra-Class PRALG_3:def 3 :

for I being non empty set

for J being ManySortedSet of I

for S being non empty non void ManySortedSign

for b_{4} being ManySortedSet of I holds

( b_{4} is MSAlgebra-Class of S,J iff for i being set st i in I holds

b_{4} . i is MSAlgebra-Family of J . i,S );

for I being non empty set

for J being ManySortedSet of I

for S being non empty non void ManySortedSign

for b

( b

b

definition

let I be non empty set ;

let S be non empty non void ManySortedSign ;

let A be MSAlgebra-Family of I,S;

let EqR be Equivalence_Relation of I;

ex b_{1} being MSAlgebra-Class of S, id (Class EqR) st

for c being set st c in Class EqR holds

b_{1} . c = A | c

for b_{1}, b_{2} being MSAlgebra-Class of S, id (Class EqR) st ( for c being set st c in Class EqR holds

b_{1} . c = A | c ) & ( for c being set st c in Class EqR holds

b_{2} . c = A | c ) holds

b_{1} = b_{2}

end;
let S be non empty non void ManySortedSign ;

let A be MSAlgebra-Family of I,S;

let EqR be Equivalence_Relation of I;

func A / EqR -> MSAlgebra-Class of S, id (Class EqR) means :Def4: :: PRALG_3:def 4

for c being set st c in Class EqR holds

it . c = A | c;

existence for c being set st c in Class EqR holds

it . c = A | c;

ex b

for c being set st c in Class EqR holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines / PRALG_3:def 4 :

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for EqR being Equivalence_Relation of I

for b_{5} being MSAlgebra-Class of S, id (Class EqR) holds

( b_{5} = A / EqR iff for c being set st c in Class EqR holds

b_{5} . c = A | c );

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for EqR being Equivalence_Relation of I

for b

( b

b

definition

let I be non empty set ;

let S be non empty non void ManySortedSign ;

let J be V8() ManySortedSet of I;

let C be MSAlgebra-Class of S,J;

ex b_{1} being MSAlgebra-Family of I,S st

for i being Element of I st i in I holds

ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st

( Ji = J . i & Cs = C . i & b_{1} . i = product Cs )

for b_{1}, b_{2} being MSAlgebra-Family of I,S st ( for i being Element of I st i in I holds

ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st

( Ji = J . i & Cs = C . i & b_{1} . i = product Cs ) ) & ( for i being Element of I st i in I holds

ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st

( Ji = J . i & Cs = C . i & b_{2} . i = product Cs ) ) holds

b_{1} = b_{2}

end;
let S be non empty non void ManySortedSign ;

let J be V8() ManySortedSet of I;

let C be MSAlgebra-Class of S,J;

func product C -> MSAlgebra-Family of I,S means :Def5: :: PRALG_3:def 5

for i being Element of I st i in I holds

ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st

( Ji = J . i & Cs = C . i & it . i = product Cs );

existence for i being Element of I st i in I holds

ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st

( Ji = J . i & Cs = C . i & it . i = product Cs );

ex b

for i being Element of I st i in I holds

ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st

( Ji = J . i & Cs = C . i & b

proof end;

uniqueness for b

ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st

( Ji = J . i & Cs = C . i & b

ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st

( Ji = J . i & Cs = C . i & b

b

proof end;

:: deftheorem Def5 defines product PRALG_3:def 5 :

for I being non empty set

for S being non empty non void ManySortedSign

for J being V8() ManySortedSet of I

for C being MSAlgebra-Class of S,J

for b_{5} being MSAlgebra-Family of I,S holds

( b_{5} = product C iff for i being Element of I st i in I holds

ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st

( Ji = J . i & Cs = C . i & b_{5} . i = product Cs ) );

for I being non empty set

for S being non empty non void ManySortedSign

for J being V8() ManySortedSet of I

for C being MSAlgebra-Class of S,J

for b

( b

ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st

( Ji = J . i & Cs = C . i & b

theorem :: PRALG_3:30

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic

proof end;