:: EXTENS_1 semantic presentation

Lemma1: for b1 being set
for b2, b3, b4 being ManySortedSet of b1
for b5 being ManySortedFunction of b2,b3
for b6 being ManySortedFunction of b3,b4 holds b6 ** b5 is ManySortedSet of b1
proof end;

theorem Th1: :: EXTENS_1:1
for b1 being Relation
for b2, b3 being set st b2 c= b3 holds
(b1 | b3) .: b2 = b1 .: b2
proof end;

theorem Th2: :: EXTENS_1:2
canceled;

theorem Th3: :: EXTENS_1:3
canceled;

theorem Th4: :: EXTENS_1:4
canceled;

theorem Th5: :: EXTENS_1:5
for b1 being set
for b2 being ManySortedSet of b1
for b3 being V3 ManySortedSet of b1
for b4 being ManySortedFunction of b2,b3
for b5 being ManySortedSubset of b2 st b2 c= b5 holds
b4 || b5 = b4
proof end;

theorem Th6: :: EXTENS_1:6
for b1 being set
for b2, b3 being ManySortedSet of b1
for b4 being ManySortedSubset of b2
for b5 being ManySortedFunction of b2,b3 holds b5 .:.: b4 c= b5 .:.: b2
proof end;

theorem Th7: :: EXTENS_1:7
for b1 being set
for b2 being ManySortedSet of b1
for b3 being V3 ManySortedSet of b1
for b4 being ManySortedFunction of b2,b3
for b5, b6 being ManySortedSubset of b2 st b5 c= b6 holds
(b4 || b6) .:.: b5 = b4 .:.: b5
proof end;

theorem Th8: :: EXTENS_1:8
for b1 being set
for b2 being ManySortedSet of b1
for b3, b4 being V3 ManySortedSet of b1
for b5 being ManySortedFunction of b2,b3
for b6 being ManySortedFunction of b3,b4
for b7 being ManySortedSubset of b2 holds (b6 ** b5) || b7 = b6 ** (b5 || b7)
proof end;

theorem Th9: :: EXTENS_1:9
for b1 being set
for b2, b3 being ManySortedSet of b1 st b2 is_transformable_to b3 holds
for b4 being ManySortedFunction of b2,b3
for b5 being ManySortedSet of b1 st b3 is ManySortedSubset of b5 holds
b4 is ManySortedFunction of b2,b5
proof end;

theorem Th10: :: EXTENS_1:10
for b1 being set
for b2 being ManySortedSet of b1
for b3 being V3 ManySortedSet of b1
for b4 being ManySortedFunction of b2,b3
for b5 being ManySortedSubset of b2 st b4 is "1-1" holds
b4 || b5 is "1-1"
proof end;

definition
let c1 be set ;
let c2 be ManySortedFunction of c1;
redefine func doms as doms c2 -> ManySortedSet of a1;
coherence
doms c2 is ManySortedSet of c1
proof end;
redefine func rngs as rngs c2 -> ManySortedSet of a1;
coherence
rngs c2 is ManySortedSet of c1
proof end;
end;

theorem Th11: :: EXTENS_1:11
for b1 being set
for b2 being ManySortedSet of b1
for b3 being V3 ManySortedSet of b1
for b4 being ManySortedFunction of b2,b3
for b5 being ManySortedSubset of b2 holds doms (b4 || b5) c= doms b4
proof end;

theorem Th12: :: EXTENS_1:12
for b1 being set
for b2 being ManySortedSet of b1
for b3 being V3 ManySortedSet of b1
for b4 being ManySortedFunction of b2,b3
for b5 being ManySortedSubset of b2 holds rngs (b4 || b5) c= rngs b4
proof end;

theorem Th13: :: EXTENS_1:13
for b1 being set
for b2, b3 being ManySortedSet of b1
for b4 being ManySortedFunction of b2,b3 holds
( b4 is "onto" iff rngs b4 = b3 )
proof end;

theorem Th14: :: EXTENS_1:14
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1 holds rngs (Reverse b2) = b2
proof end;

theorem Th15: :: EXTENS_1:15
for b1 being set
for b2 being ManySortedSet of b1
for b3, b4 being V3 ManySortedSet of b1
for b5 being ManySortedFunction of b2,b3
for b6 being ManySortedFunction of b3,b4
for b7 being V3 ManySortedSubset of b3 st rngs b5 c= b7 holds
(b6 || b7) ** b5 = b6 ** b5
proof end;

theorem Th16: :: EXTENS_1:16
for b1 being set
for b2 being ManySortedSet of b1
for b3 being V3 ManySortedSet of b1
for b4 being ManySortedFunction of b2,b3 holds
( b4 is "onto" iff for b5 being V3 ManySortedSet of b1
for b6, b7 being ManySortedFunction of b3,b5 st b6 ** b4 = b7 ** b4 holds
b6 = b7 )
proof end;

theorem Th17: :: EXTENS_1:17
for b1 being set
for b2 being ManySortedSet of b1
for b3 being V3 ManySortedSet of b1
for b4 being ManySortedFunction of b2,b3 st b2 is non-empty & b3 is non-empty holds
( b4 is "1-1" iff for b5 being ManySortedSet of b1
for b6, b7 being ManySortedFunction of b5,b2 st b4 ** b6 = b4 ** b7 holds
b6 = b7 )
proof end;

theorem Th18: :: EXTENS_1:18
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being V3 ManySortedSet of the carrier of b1
for b4, b5 being ManySortedFunction of (FreeMSA b3),b2 st b4 is_homomorphism FreeMSA b3,b2 & b5 is_homomorphism FreeMSA b3,b2 & b4 || (FreeGen b3) = b5 || (FreeGen b3) holds
b4 = b5
proof end;

theorem Th19: :: EXTENS_1:19
for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is_homomorphism b2,b3 & b4 is_epimorphism b2,b3 holds
for b5 being non-empty MSAlgebra of b1
for b6, b7 being ManySortedFunction of b3,b5 st b6 is_homomorphism b3,b5 & b7 is_homomorphism b3,b5 & b6 ** b4 = b7 ** b4 holds
b6 = b7
proof end;

theorem Th20: :: EXTENS_1:20
for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is_homomorphism b2,b3 holds
( b4 is_monomorphism b2,b3 iff for b5 being non-empty MSAlgebra of b1
for b6, b7 being ManySortedFunction of b5,b2 st b6 is_homomorphism b5,b2 & b7 is_homomorphism b5,b2 & b4 ** b6 = b4 ** b7 holds
b6 = b7 )
proof end;

registration
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
cluster V3 GeneratorSet of a2;
existence
ex b1 being GeneratorSet of c2 st b1 is non-empty
proof end;
end;

theorem Th21: :: EXTENS_1:21
for b1 being non empty non void ManySortedSign
for b2 being MSAlgebra of b1
for b3, b4 being MSSubset of b2 st b3 is ManySortedSubset of b4 holds
GenMSAlg b3 is MSSubAlgebra of GenMSAlg b4
proof end;

theorem Th22: :: EXTENS_1:22
for b1 being non empty non void ManySortedSign
for b2 being MSAlgebra of b1
for b3 being MSSubAlgebra of b2
for b4 being MSSubset of b2
for b5 being MSSubset of b3 st b4 = b5 holds
GenMSAlg b4 = GenMSAlg b5
proof end;

theorem Th23: :: EXTENS_1:23
for b1 being non empty non void ManySortedSign
for b2 being strict non-empty MSAlgebra of b1
for b3 being non-empty MSAlgebra of b1
for b4 being GeneratorSet of b2
for b5, b6 being ManySortedFunction of b2,b3 st b5 is_homomorphism b2,b3 & b6 is_homomorphism b2,b3 & b5 || b4 = b6 || b4 holds
b5 = b6
proof end;