let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for a1, a2 being FinSequence st a1 in Args (o,(TermAlg S)) & a2 in Args (o,(TermAlg S)) & ( for i being Nat st i in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . i holds
for t1, t2 being Element of (TermAlg S),s st t1 = a1 . i & t2 = a2 . i holds
A |= t1 '=' t2 ) holds
for t1, t2 being Element of (TermAlg S),(the_result_sort_of o) st t1 = [o, the carrier of S] -tree a1 & t2 = [o, the carrier of S] -tree a2 holds
A |= t1 '=' t2
let A be non-empty MSAlgebra over S; for o being OperSymbol of S
for a1, a2 being FinSequence st a1 in Args (o,(TermAlg S)) & a2 in Args (o,(TermAlg S)) & ( for i being Nat st i in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . i holds
for t1, t2 being Element of (TermAlg S),s st t1 = a1 . i & t2 = a2 . i holds
A |= t1 '=' t2 ) holds
for t1, t2 being Element of (TermAlg S),(the_result_sort_of o) st t1 = [o, the carrier of S] -tree a1 & t2 = [o, the carrier of S] -tree a2 holds
A |= t1 '=' t2
let o be OperSymbol of S; for a1, a2 being FinSequence st a1 in Args (o,(TermAlg S)) & a2 in Args (o,(TermAlg S)) & ( for i being Nat st i in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . i holds
for t1, t2 being Element of (TermAlg S),s st t1 = a1 . i & t2 = a2 . i holds
A |= t1 '=' t2 ) holds
for t1, t2 being Element of (TermAlg S),(the_result_sort_of o) st t1 = [o, the carrier of S] -tree a1 & t2 = [o, the carrier of S] -tree a2 holds
A |= t1 '=' t2
let a1, a2 be FinSequence; ( a1 in Args (o,(TermAlg S)) & a2 in Args (o,(TermAlg S)) & ( for i being Nat st i in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . i holds
for t1, t2 being Element of (TermAlg S),s st t1 = a1 . i & t2 = a2 . i holds
A |= t1 '=' t2 ) implies for t1, t2 being Element of (TermAlg S),(the_result_sort_of o) st t1 = [o, the carrier of S] -tree a1 & t2 = [o, the carrier of S] -tree a2 holds
A |= t1 '=' t2 )
assume A1:
a1 in Args (o,(TermAlg S))
; ( not a2 in Args (o,(TermAlg S)) or ex i being Nat st
( i in dom (the_arity_of o) & ex s being SortSymbol of S st
( s = (the_arity_of o) . i & ex t1, t2 being Element of (TermAlg S),s st
( t1 = a1 . i & t2 = a2 . i & not A |= t1 '=' t2 ) ) ) or for t1, t2 being Element of (TermAlg S),(the_result_sort_of o) st t1 = [o, the carrier of S] -tree a1 & t2 = [o, the carrier of S] -tree a2 holds
A |= t1 '=' t2 )
assume A2:
a2 in Args (o,(TermAlg S))
; ( ex i being Nat st
( i in dom (the_arity_of o) & ex s being SortSymbol of S st
( s = (the_arity_of o) . i & ex t1, t2 being Element of (TermAlg S),s st
( t1 = a1 . i & t2 = a2 . i & not A |= t1 '=' t2 ) ) ) or for t1, t2 being Element of (TermAlg S),(the_result_sort_of o) st t1 = [o, the carrier of S] -tree a1 & t2 = [o, the carrier of S] -tree a2 holds
A |= t1 '=' t2 )
then reconsider b1 = a1, b2 = a2 as Element of Args (o,(TermAlg S)) by A1;
assume A3:
for i being Nat st i in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . i holds
for t1, t2 being Element of (TermAlg S),s st t1 = a1 . i & t2 = a2 . i holds
A |= t1 '=' t2
; for t1, t2 being Element of (TermAlg S),(the_result_sort_of o) st t1 = [o, the carrier of S] -tree a1 & t2 = [o, the carrier of S] -tree a2 holds
A |= t1 '=' t2
set s = the_result_sort_of o;
let t1, t2 be Element of (TermAlg S),(the_result_sort_of o); ( t1 = [o, the carrier of S] -tree a1 & t2 = [o, the carrier of S] -tree a2 implies A |= t1 '=' t2 )
assume A4:
t1 = [o, the carrier of S] -tree a1
; ( not t2 = [o, the carrier of S] -tree a2 or A |= t1 '=' t2 )
assume A5:
t2 = [o, the carrier of S] -tree a2
; A |= t1 '=' t2
let h be ManySortedFunction of (TermAlg S),A; EQUATION:def 5 ( not h is_homomorphism TermAlg S,A or (h . (the_result_sort_of o)) . ((t1 '=' t2) `1) = (h . (the_result_sort_of o)) . ((t1 '=' t2) `2) )
assume A6:
h is_homomorphism TermAlg S,A
; (h . (the_result_sort_of o)) . ((t1 '=' t2) `1) = (h . (the_result_sort_of o)) . ((t1 '=' t2) `2)
A7:
now for n being Nat st n in dom b1 holds
(h # b2) . n = (h . ((the_arity_of o) /. n)) . (b1 . n)let n be
Nat;
( n in dom b1 implies (h # b2) . n = (h . ((the_arity_of o) /. n)) . (b1 . n) )assume A8:
n in dom b1
;
(h # b2) . n = (h . ((the_arity_of o) /. n)) . (b1 . n)A9:
(
dom b1 = dom (the_arity_of o) &
dom b2 = dom (the_arity_of o) )
by MSUALG_3:6;
reconsider s =
(the_arity_of o) . n as
SortSymbol of
S by A8, A9, FUNCT_1:102;
(
dom ( the Sorts of (TermAlg S) * (the_arity_of o)) = dom (the_arity_of o) &
( the Sorts of (TermAlg S) * (the_arity_of o)) . n = the
Sorts of
(TermAlg S) . s )
by A8, A9, FUNCT_1:13, PRALG_2:3;
then reconsider t1 =
a1 . n,
t2 =
a2 . n as
Element of
(TermAlg S),
s by A8, A9, MSUALG_3:6;
(h . s) . ((t1 '=' t2) `1) = (h . s) . ((t1 '=' t2) `2)
by A3, A8, A9, A6, EQUATION:def 5;
then A10:
(h . s) . t1 =
(h . s) . ((t1 '=' t2) `2)
.=
(h . s) . t2
;
A11:
s = (the_arity_of o) /. n
by A8, A9, PARTFUN1:def 6;
thus
(h # b2) . n = (h . ((the_arity_of o) /. n)) . (b1 . n)
by A10, A11, A8, A9, MSUALG_3:def 6;
verum end;
thus (h . (the_result_sort_of o)) . ((t1 '=' t2) `1) =
(h . (the_result_sort_of o)) . ((Den (o,(TermAlg S))) . a1)
by A1, A4, INSTALG1:3
.=
(Den (o,A)) . (h # b1)
by A6
.=
(Den (o,A)) . (h # b2)
by A7, MSUALG_3:def 6
.=
(h . (the_result_sort_of o)) . ((Den (o,(TermAlg S))) . a2)
by A6
.=
(h . (the_result_sort_of o)) . ((t1 '=' t2) `2)
by A2, A5, INSTALG1:3
; verum