let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: ( 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)) ; :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( 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 ; :: thesis: ( not t2 = [o, the carrier of S] -tree a2 or A |= t1 '=' t2 )
assume A5: t2 = [o, the carrier of S] -tree a2 ; :: thesis: A |= t1 '=' t2
let h be ManySortedFunction of (TermAlg S),A; :: according to EQUATION:def 5 :: thesis: ( 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 ; :: thesis: (h . (the_result_sort_of o)) . ((t1 '=' t2) `1) = (h . (the_result_sort_of o)) . ((t1 '=' t2) `2)

A7: now :: thesis: 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; :: thesis: ( n in dom b1 implies (h # b2) . n = (h . ((the_arity_of o) /. n)) . (b1 . n) )
assume A8: n in dom b1 ; :: thesis: (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; :: thesis: 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 ; :: thesis: verum