:: PRALG_3 semantic presentation

registration

let I be set ;
let S be non empty non void ManySortedSign ;
let AF be MSAlgebra-Family of I,S;
cluster product AF -> non-empty ;
coherence by MSUALG_1:def 8;

end;

definition

let I be set ;
:: original: id
redefine func id I -> ManySortedSet of I;
coherence

proof end;

end;

registration

let X be with_non-empty_elements set ;
cluster id X -> non-empty ;
coherence

proof end;

end;

theorem Th1: :: PRALG_3:1

for f, F being Function
for A being set st f in product F holds
f | A in product (F | A)

proof 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

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

proof end;

Lm1: for f being Function
for x being set st x in product f holds
x is Function

proof end;

theorem :: PRALG_3:4

canceled;

theorem :: PRALG_3:5

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 d in dom F & 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 of S;
let o be OperSymbol of S;
func const o,U0 -> set equals :: PRALG_3:def 1
(Den o,U0) . {} ;
correctness ;

end;

:: deftheorem defines const PRALG_3:def 1 :

theorem Th6: :: PRALG_3:6

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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:7

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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 OperSymbols of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }

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
(commute (OPER A)) . o in Funcs I,(Funcs {{} },(union { (Result o,(A . i')) where i' is Element of I : verum } ))

proof end;

theorem Th9: :: PRALG_3:9

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 . i')) where i' 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;
cluster const o,(product A) -> Relation-like Function-like ;
coherence

proof end;

end;

theorem Th10: :: PRALG_3:10

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)

proof end;

theorem :: PRALG_3:11

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)

proof end;

theorem Th12: :: PRALG_3:12

for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of 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 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 of 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 Th14: :: PRALG_3:14

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) holds x in Funcs (dom (the_arity_of o)),(Funcs I,(union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } ))

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 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 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 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 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
commute y in product (doms (A ?. o))

proof end;

theorem Th19: :: PRALG_3:19

proof end;

theorem Th20: :: PRALG_3:20

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))

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 st the_arity_of o <> {} holds
for U1 being non-empty MSAlgebra of S
for x being Element of Args o,(product A) holds (commute x) . i is Element of Args o,(A . 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 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 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 st the_arity_of o <> {} holds
for y being Element of Args o,(product A)
for i' being Element of I
for g being Function st g = (Den o,(product A)) . y holds
g . i' = (Den o,(A . i')) . ((commute y) . i')

proof end;

definition

let f be Function;
let x be set ;
func proj f,x -> Function means :Def2: :: PRALG_3:def 2
( dom it = product f & ( for y being Function st y in dom it holds
it . y = y . x ) );
existence

proof end;

uniqueness

proof end;

end;

:: 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines proj PRALG_3:def 3 :

theorem Th24: :: PRALG_3:24

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 Args o,(product A) <> {} & the_arity_of o <> {} holds
for i being Element of I holds (proj A,i) # x = (commute x) . i

proof end;

theorem :: 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 holds proj A,i is_homomorphism product A,A . i

proof end;

theorem Th26: :: PRALG_3:26

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 of 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 . i') . s1) where s1 is SortSymbol of S, i' is Element of I : verum } ) & ((commute F) . s) . i = (F . i) . s )

proof end;

theorem Th27: :: PRALG_3:27

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 of 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 . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum } ))

proof end;

theorem Th28: :: PRALG_3:28

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 of 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 F' being ManySortedFunction of U1,(A . i) st F' = 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 = (F' . s) . x

proof end;

theorem Th29: :: 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 s being SortSymbol of S
for U1 being non-empty MSAlgebra of 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:30

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 of 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 ;
mode MSAlgebra-Class of S,J -> ManySortedSet of I means :Def4: :: PRALG_3:def 4
for i being set st i in I holds
it . i is MSAlgebra-Family of J . i,S;
existence

proof end;

end;

:: deftheorem Def4 defines MSAlgebra-Class PRALG_3:def 4 :

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;
func A / EqR -> MSAlgebra-Class of S, id (Class EqR) means :Def5: :: PRALG_3:def 5
for c being set st c in Class EqR holds
it . c = A | c;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines / PRALG_3:def 5 :

definition

let I be non empty set ;
let S be non empty non void ManySortedSign ;
let J be V2 ManySortedSet of I;
let C be MSAlgebra-Class of S,J;
func product C -> MSAlgebra-Family of I,S means :Def6: :: PRALG_3:def 6
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines product PRALG_3:def 6 :

theorem :: PRALG_3:31

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

proof end;