:: PRALG_3 semantic presentation

registration
let c1 be set ;
let c2 be non empty non void ManySortedSign ;
let c3 be MSAlgebra-Family of c1,c2;
cluster product a3 -> non-empty ;
coherence
product c3 is non-empty by MSUALG_1:def 8;
end;

definition
let c1 be set ;
redefine func id as id c1 -> ManySortedSet of a1;
coherence
id c1 is ManySortedSet of c1
proof end;
end;

registration
let c1 be with_non-empty_elements set ;
cluster id a1 -> non-empty ;
coherence
id c1 is non-empty
proof end;
end;

theorem Th1: :: PRALG_3:1
for b1, b2 being Function
for b3 being set st b1 in product b2 holds
b1 | b3 in product (b2 | b3)
proof end;

theorem Th2: :: PRALG_3:2
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being SortSymbol of b2
for b5 being non empty Subset of b1
for b6 being MSAlgebra-Family of b5,b2 st b3 | b5 = b6 holds
Carrier b6,b4 = (Carrier b3,b4) | b5
proof end;

theorem Th3: :: PRALG_3:3
for b1 being set
for b2 being non empty set
for b3 being Equivalence_Relation of b2
for b4, b5 being Element of Class b3 st b1 in b4 & b1 in b5 holds
b4 = b5
proof end;

Lemma4: for b1 being Function
for b2 being set st b2 in product b1 holds
b2 is Function
proof end;

theorem Th4: :: PRALG_3:4
canceled;

theorem Th5: :: PRALG_3:5
for b1 being non empty set
for b2 being ManySortedFunction of b1
for b3 being non empty functional with_common_domain set st b3 = rng b2 holds
for b4 being Element of b1
for b5 being set st b4 in dom b2 & b5 in DOM b3 holds
(b2 . b4) . b5 = ((commute b2) . b5) . b4
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be MSAlgebra of c1;
let c3 be OperSymbol of c1;
func const c3,c2 -> set equals :: PRALG_3:def 1
(Den a3,a2) . {} ;
correctness
coherence
(Den c3,c2) . {} is set ;
;
end;

:: deftheorem Def1 defines const PRALG_3:def 1 :
for b1 being non empty non void ManySortedSign
for b2 being MSAlgebra of b1
for b3 being OperSymbol of b1 holds const b3,b2 = (Den b3,b2) . {} ;

theorem Th6: :: PRALG_3:6
for b1 being non empty non void ManySortedSign
for b2 being MSAlgebra of b1
for b3 being OperSymbol of b1 st the_arity_of b3 = {} & Result b3,b2 <> {} holds
const b3,b2 in Result b3,b2
proof end;

theorem Th7: :: PRALG_3:7
for b1 being non empty non void ManySortedSign
for b2 being MSAlgebra of b1
for b3 being SortSymbol of b1 st the Sorts of b2 . b3 <> {} holds
Constants b2,b3 = { (const b4,b2) where B is Element of the OperSymbols of b1 : ( the_result_sort_of b4 = b3 & the_arity_of b4 = {} ) }
proof end;

theorem Th8: :: PRALG_3:8
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being OperSymbol of b2 st the_arity_of b4 = {} holds
(commute (OPER b3)) . b4 in Funcs b1,(Funcs {{} },(union { (Result b4,(b3 . b5)) where B is Element of b1 : verum } ))
proof end;

theorem Th9: :: PRALG_3:9
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being OperSymbol of b2 st the_arity_of b4 = {} holds
const b4,(product b3) in Funcs b1,(union { (Result b4,(b3 . b5)) where B is Element of b1 : verum } )
proof end;

registration
let c1 be non empty non void ManySortedSign ;
let c2 be non empty set ;
let c3 be OperSymbol of c1;
let c4 be MSAlgebra-Family of c2,c1;
cluster const a3,(product a4) -> Relation-like Function-like ;
coherence
( const c3,(product c4) is Relation-like & const c3,(product c4) is Function-like )
proof end;
end;

theorem Th10: :: PRALG_3:10
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being Element of b1
for b4 being MSAlgebra-Family of b1,b2
for b5 being OperSymbol of b2 st the_arity_of b5 = {} holds
(const b5,(product b4)) . b3 = const b5,(b4 . b3)
proof end;

theorem Th11: :: PRALG_3:11
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being OperSymbol of b2
for b5 being Function st the_arity_of b4 = {} & dom b5 = b1 & ( for b6 being Element of b1 holds b5 . b6 = const b4,(b3 . b6) ) holds
b5 = const b4,(product b3)
proof end;

theorem Th12: :: PRALG_3:12
for b1 being non empty non void ManySortedSign
for b2, b3 being MSAlgebra of b1
for b4 being OperSymbol of b1
for b5 being Element of Args b4,b2 st b5 = {} & the_arity_of b4 = {} & Args b4,b2 <> {} & Args b4,b3 <> {} holds
for b6 being ManySortedFunction of b2,b3 holds b6 # b5 = {}
proof end;

theorem Th13: :: PRALG_3:13
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3, b4 being non-empty MSAlgebra of b1
for b5 being ManySortedFunction of b3,b4
for b6 being Element of Args b2,b3 holds b6 in product (doms (b5 * (the_arity_of b2)))
proof end;

theorem Th14: :: PRALG_3:14
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3, b4 being non-empty MSAlgebra of b1
for b5 being ManySortedFunction of b3,b4
for b6 being Element of Args b2,b3
for b7 being set st b7 in dom (the_arity_of b2) holds
(b5 # b6) . b7 = (b5 . ((the_arity_of b2) /. b7)) . (b6 . b7)
proof end;

theorem Th15: :: PRALG_3:15
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being OperSymbol of b2
for b5 being Element of Args b4,(product b3) holds b5 in Funcs (dom (the_arity_of b4)),(Funcs b1,(union { (the Sorts of (b3 . b6) . b7) where B is Element of b1, B is Element of the carrier of b2 : verum } ))
proof end;

theorem Th16: :: PRALG_3:16
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being OperSymbol of b2
for b5 being Element of Args b4,(product b3)
for b6 being set st b6 in dom (the_arity_of b4) holds
b5 . b6 in product (Carrier b3,((the_arity_of b4) /. b6))
proof end;

theorem Th17: :: PRALG_3:17
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being OperSymbol of b2
for b5 being Element of b1
for b6 being set st b6 in dom (the_arity_of b4) holds
for b7 being SortSymbol of b2 st b7 = (the_arity_of b4) . b6 holds
for b8 being Element of Args b4,(product b3)
for b9 being Function st b9 = b8 . b6 holds
b9 . b5 in the Sorts of (b3 . b5) . b7
proof end;

theorem Th18: :: PRALG_3:18
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being OperSymbol of b2
for b5 being Element of Args b4,(product b3) st the_arity_of b4 <> {} holds
commute b5 in product (doms (b3 ?. b4))
proof end;

theorem Th19: :: PRALG_3:19
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being OperSymbol of b2
for b5 being Element of Args b4,(product b3) st the_arity_of b4 <> {} holds
b5 in dom (Commute (Frege (b3 ?. b4)))
proof end;

theorem Th20: :: PRALG_3:20
for b1 being set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being OperSymbol of b2
for b5 being Element of Args b4,(product b3) holds (Den b4,(product b3)) . b5 in product (Carrier b3,(the_result_sort_of b4))
proof end;

theorem Th21: :: PRALG_3:21
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being Element of b1
for b5 being OperSymbol of b2 st the_arity_of b5 <> {} holds
for b6 being non-empty MSAlgebra of b2
for b7 being Element of Args b5,(product b3) holds (commute b7) . b4 is Element of Args b5,(b3 . b4)
proof end;

theorem Th22: :: PRALG_3:22
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being Element of b1
for b5 being OperSymbol of b2
for b6 being Element of Args b5,(product b3)
for b7 being set st b7 in dom (the_arity_of b5) holds
for b8 being Function st b8 = b6 . b7 holds
((commute b6) . b4) . b7 = b8 . b4
proof end;

theorem Th23: :: PRALG_3:23
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being OperSymbol of b2 st the_arity_of b4 <> {} holds
for b5 being Element of Args b4,(product b3)
for b6 being Element of b1
for b7 being Function st b7 = (Den b4,(product b3)) . b5 holds
b7 . b6 = (Den b4,(b3 . b6)) . ((commute b5) . b6)
proof end;

definition
let c1 be Function;
let c2 be set ;
func proj c1,c2 -> Function means :Def2: :: PRALG_3:def 2
( dom a3 = product a1 & ( for b1 being Function st b1 in dom a3 holds
a3 . b1 = b1 . a2 ) );
existence
ex b1 being Function st
( dom b1 = product c1 & ( for b2 being Function st b2 in dom b1 holds
b1 . b2 = b2 . c2 ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = product c1 & ( for b3 being Function st b3 in dom b1 holds
b1 . b3 = b3 . c2 ) & dom b2 = product c1 & ( for b3 being Function st b3 in dom b2 holds
b2 . b3 = b3 . c2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines proj PRALG_3:def 2 :
for b1 being Function
for b2 being set
for b3 being Function holds
( b3 = proj b1,b2 iff ( dom b3 = product b1 & ( for b4 being Function st b4 in dom b3 holds
b3 . b4 = b4 . b2 ) ) );

definition
let c1 be non empty set ;
let c2 be non empty non void ManySortedSign ;
let c3 be MSAlgebra-Family of c1,c2;
let c4 be Element of c1;
func proj c3,c4 -> ManySortedFunction of (product a3),(a3 . a4) means :Def3: :: PRALG_3:def 3
for b1 being Element of a2 holds a5 . b1 = proj (Carrier a3,b1),a4;
existence
ex b1 being ManySortedFunction of (product c3),(c3 . c4) st
for b2 being Element of c2 holds b1 . b2 = proj (Carrier c3,b2),c4
proof end;
uniqueness
for b1, b2 being ManySortedFunction of (product c3),(c3 . c4) st ( for b3 being Element of c2 holds b1 . b3 = proj (Carrier c3,b3),c4 ) & ( for b3 being Element of c2 holds b2 . b3 = proj (Carrier c3,b3),c4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines proj PRALG_3:def 3 :
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being Element of b1
for b5 being ManySortedFunction of (product b3),(b3 . b4) holds
( b5 = proj b3,b4 iff for b6 being Element of b2 holds b5 . b6 = proj (Carrier b3,b6),b4 );

theorem Th24: :: PRALG_3:24
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being OperSymbol of b2
for b5 being Element of Args b4,(product b3) st Args b4,(product b3) <> {} & the_arity_of b4 <> {} holds
for b6 being Element of b1 holds (proj b3,b6) # b5 = (commute b5) . b6
proof end;

theorem Th25: :: PRALG_3:25
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being Element of b1
for b4 being MSAlgebra-Family of b1,b2 holds proj b4,b3 is_homomorphism product b4,b4 . b3
proof end;

theorem Th26: :: PRALG_3:26
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being Element of b1
for b4 being MSAlgebra-Family of b1,b2
for b5 being SortSymbol of b2
for b6 being non-empty MSAlgebra of b2
for b7 being ManySortedFunction of b1 st ( for b8 being Element of b1 ex b9 being ManySortedFunction of b6,(b4 . b8) st
( b9 = b7 . b8 & b9 is_homomorphism b6,b4 . b8 ) ) holds
( b7 in Funcs b1,(Funcs the carrier of b2,{ ((b7 . b9) . b8) where B is SortSymbol of b2, B is Element of b1 : verum } ) & ((commute b7) . b5) . b3 = (b7 . b3) . b5 )
proof end;

theorem Th27: :: PRALG_3:27
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being SortSymbol of b2
for b5 being non-empty MSAlgebra of b2
for b6 being ManySortedFunction of b1 st ( for b7 being Element of b1 ex b8 being ManySortedFunction of b5,(b3 . b7) st
( b8 = b6 . b7 & b8 is_homomorphism b5,b3 . b7 ) ) holds
(commute b6) . b4 in Funcs b1,(Funcs (the Sorts of b5 . b4),(union { (the Sorts of (b3 . b7) . b8) where B is Element of b1, B is SortSymbol of b2 : verum } ))
proof end;

theorem Th28: :: PRALG_3:28
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being Element of b1
for b4 being MSAlgebra-Family of b1,b2
for b5 being SortSymbol of b2
for b6 being non-empty MSAlgebra of b2
for b7 being ManySortedFunction of b1 st ( for b8 being Element of b1 ex b9 being ManySortedFunction of b6,(b4 . b8) st
( b9 = b7 . b8 & b9 is_homomorphism b6,b4 . b8 ) ) holds
for b8 being ManySortedFunction of b6,(b4 . b3) st b8 = b7 . b3 holds
for b9 being set st b9 in the Sorts of b6 . b5 holds
for b10 being Function st b10 = (commute ((commute b7) . b5)) . b9 holds
b10 . b3 = (b8 . b5) . b9
proof end;

theorem Th29: :: PRALG_3:29
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being SortSymbol of b2
for b5 being non-empty MSAlgebra of b2
for b6 being ManySortedFunction of b1 st ( for b7 being Element of b1 ex b8 being ManySortedFunction of b5,(b3 . b7) st
( b8 = b6 . b7 & b8 is_homomorphism b5,b3 . b7 ) ) holds
for b7 being set st b7 in the Sorts of b5 . b4 holds
(commute ((commute b6) . b4)) . b7 in product (Carrier b3,b4)
proof end;

theorem Th30: :: PRALG_3:30
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being non-empty MSAlgebra of b2
for b5 being ManySortedFunction of b1 st ( for b6 being Element of b1 ex b7 being ManySortedFunction of b4,(b3 . b6) st
( b7 = b5 . b6 & b7 is_homomorphism b4,b3 . b6 ) ) holds
ex b6 being ManySortedFunction of b4,(product b3) st
( b6 is_homomorphism b4, product b3 & ( for b7 being Element of b1 holds (proj b3,b7) ** b6 = b5 . b7 ) )
proof end;

definition
let c1 be non empty set ;
let c2 be ManySortedSet of c1;
let c3 be non empty non void ManySortedSign ;
mode MSAlgebra-Class of c3,c2 -> ManySortedSet of a1 means :Def4: :: PRALG_3:def 4
for b1 being set st b1 in a1 holds
a4 . b1 is MSAlgebra-Family of a2 . b1,a3;
existence
ex b1 being ManySortedSet of c1 st
for b2 being set st b2 in c1 holds
b1 . b2 is MSAlgebra-Family of c2 . b2,c3
proof end;
end;

:: deftheorem Def4 defines MSAlgebra-Class PRALG_3:def 4 :
for b1 being non empty set
for b2 being ManySortedSet of b1
for b3 being non empty non void ManySortedSign
for b4 being ManySortedSet of b1 holds
( b4 is MSAlgebra-Class of b3,b2 iff for b5 being set st b5 in b1 holds
b4 . b5 is MSAlgebra-Family of b2 . b5,b3 );

definition
let c1 be non empty set ;
let c2 be non empty non void ManySortedSign ;
let c3 be MSAlgebra-Family of c1,c2;
let c4 be Equivalence_Relation of c1;
func c3 / c4 -> MSAlgebra-Class of a2, id (Class a4) means :Def5: :: PRALG_3:def 5
for b1 being set st b1 in Class a4 holds
a5 . b1 = a3 | b1;
existence
ex b1 being MSAlgebra-Class of c2, id (Class c4) st
for b2 being set st b2 in Class c4 holds
b1 . b2 = c3 | b2
proof end;
uniqueness
for b1, b2 being MSAlgebra-Class of c2, id (Class c4) st ( for b3 being set st b3 in Class c4 holds
b1 . b3 = c3 | b3 ) & ( for b3 being set st b3 in Class c4 holds
b2 . b3 = c3 | b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines / PRALG_3:def 5 :
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being Equivalence_Relation of b1
for b5 being MSAlgebra-Class of b2, id (Class b4) holds
( b5 = b3 / b4 iff for b6 being set st b6 in Class b4 holds
b5 . b6 = b3 | b6 );

definition
let c1 be non empty set ;
let c2 be non empty non void ManySortedSign ;
let c3 be V2 ManySortedSet of c1;
let c4 be MSAlgebra-Class of c2,c3;
func product c4 -> MSAlgebra-Family of a1,a2 means :Def6: :: PRALG_3:def 6
for b1 being Element of a1 st b1 in a1 holds
ex b2 being non empty set ex b3 being MSAlgebra-Family of b2,a2 st
( b2 = a3 . b1 & b3 = a4 . b1 & a5 . b1 = product b3 );
existence
ex b1 being MSAlgebra-Family of c1,c2 st
for b2 being Element of c1 st b2 in c1 holds
ex b3 being non empty set ex b4 being MSAlgebra-Family of b3,c2 st
( b3 = c3 . b2 & b4 = c4 . b2 & b1 . b2 = product b4 )
proof end;
uniqueness
for b1, b2 being MSAlgebra-Family of c1,c2 st ( for b3 being Element of c1 st b3 in c1 holds
ex b4 being non empty set ex b5 being MSAlgebra-Family of b4,c2 st
( b4 = c3 . b3 & b5 = c4 . b3 & b1 . b3 = product b5 ) ) & ( for b3 being Element of c1 st b3 in c1 holds
ex b4 being non empty set ex b5 being MSAlgebra-Family of b4,c2 st
( b4 = c3 . b3 & b5 = c4 . b3 & b2 . b3 = product b5 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines product PRALG_3:def 6 :
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being V2 ManySortedSet of b1
for b4 being MSAlgebra-Class of b2,b3
for b5 being MSAlgebra-Family of b1,b2 holds
( b5 = product b4 iff for b6 being Element of b1 st b6 in b1 holds
ex b7 being non empty set ex b8 being MSAlgebra-Family of b7,b2 st
( b7 = b3 . b6 & b8 = b4 . b6 & b5 . b6 = product b8 ) );

theorem Th31: :: PRALG_3:31
for b1 being non empty set
for b2 being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of b1,b2
for b4 being Equivalence_Relation of b1 holds product b3, product (product (b3 / b4)) are_isomorphic
proof end;