let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of S
for A, B being non-empty b1,S -terms MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
( ( A is all_vars_including implies B is all_vars_including ) & ( A is inheriting_operations implies B is inheriting_operations ) & ( A is free_in_itself implies B is free_in_itself ) )
let X be V5() ManySortedSet of S; for A, B being non-empty X,S -terms MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
( ( A is all_vars_including implies B is all_vars_including ) & ( A is inheriting_operations implies B is inheriting_operations ) & ( A is free_in_itself implies B is free_in_itself ) )
let A, B be non-empty X,S -terms MSAlgebra over S; ( MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) implies ( ( A is all_vars_including implies B is all_vars_including ) & ( A is inheriting_operations implies B is inheriting_operations ) & ( A is free_in_itself implies B is free_in_itself ) ) )
assume A1:
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
; ( ( A is all_vars_including implies B is all_vars_including ) & ( A is inheriting_operations implies B is inheriting_operations ) & ( A is free_in_itself implies B is free_in_itself ) )
thus
( A is all_vars_including implies B is all_vars_including )
by A1; ( ( A is inheriting_operations implies B is inheriting_operations ) & ( A is free_in_itself implies B is free_in_itself ) )
thus
( A is inheriting_operations implies B is inheriting_operations )
( A is free_in_itself implies B is free_in_itself )proof
assume A3:
for
o being
OperSymbol of
S for
p being
FinSequence st
p in Args (
o,
(Free (S,X))) &
(Den (o,(Free (S,X)))) . p in the
Sorts of
A . (the_result_sort_of o) holds
(
p in Args (
o,
A) &
(Den (o,A)) . p = (Den (o,(Free (S,X)))) . p )
;
MSAFREE4:def 8 B is inheriting_operations
let o be
OperSymbol of
S;
MSAFREE4:def 8 for p being FinSequence st p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of B . (the_result_sort_of o) holds
( p in Args (o,B) & (Den (o,B)) . p = (Den (o,(Free (S,X)))) . p )let p be
FinSequence;
( p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of B . (the_result_sort_of o) implies ( p in Args (o,B) & (Den (o,B)) . p = (Den (o,(Free (S,X)))) . p ) )
(
Args (
o,
A)
= Args (
o,
B) &
Den (
o,
A)
= Den (
o,
B) )
by A1;
hence
(
p in Args (
o,
(Free (S,X))) &
(Den (o,(Free (S,X)))) . p in the
Sorts of
B . (the_result_sort_of o) implies (
p in Args (
o,
B) &
(Den (o,B)) . p = (Den (o,(Free (S,X)))) . p ) )
by A1, A3;
verum
end;
assume A4:
for f being ManySortedFunction of FreeGen X, the Sorts of A
for G being ManySortedSubset of the Sorts of A st G = FreeGen X holds
ex h being ManySortedFunction of A,A st
( h is_homomorphism A,A & f = h || G )
; MSAFREE4:def 9 B is free_in_itself
let f be ManySortedFunction of FreeGen X, the Sorts of B; MSAFREE4:def 9 for G being ManySortedSubset of the Sorts of B st G = FreeGen X holds
ex h being ManySortedFunction of B,B st
( h is_homomorphism B,B & f = h || G )
let G be ManySortedSubset of the Sorts of B; ( G = FreeGen X implies ex h being ManySortedFunction of B,B st
( h is_homomorphism B,B & f = h || G ) )
assume A5:
G = FreeGen X
; ex h being ManySortedFunction of B,B st
( h is_homomorphism B,B & f = h || G )
reconsider G1 = G as ManySortedSubset of the Sorts of A by A1;
consider h being ManySortedFunction of A,A such that
A6:
( h is_homomorphism A,A & f = h || G1 )
by A1, A4, A5;
reconsider h2 = h as ManySortedFunction of B,B by A1;
take
h2
; ( h2 is_homomorphism B,B & f = h2 || G )
thus
h2 is_homomorphism B,B
by A6, A1, Th30; f = h2 || G
thus
f = h2 || G
by A1, A6; verum