let S be non empty non void ManySortedSign ; :: thesis: for X0 being V5() countable ManySortedSet of S
for A0 being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for w being ManySortedFunction of X0, the carrier of S --> NAT
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X0)))
for q being Element of Args (o,A0) st (canonical_homomorphism A0) # p = q holds
for t1, t2 being Term of S,X0 st t1 = (Den (o,(Free (S,X0)))) . p & t2 = (Den (o,A0)) . q holds
for t3, t4 being Element of (TermAlg S),(the_result_sort_of o) st t3 = # (t1,w) & t4 = # (t2,w) holds
A0 |= t3 '=' t4
let X0 be V5() countable ManySortedSet of S; :: thesis: for A0 being X0,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for w being ManySortedFunction of X0, the carrier of S --> NAT
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X0)))
for q being Element of Args (o,A0) st (canonical_homomorphism A0) # p = q holds
for t1, t2 being Term of S,X0 st t1 = (Den (o,(Free (S,X0)))) . p & t2 = (Den (o,A0)) . q holds
for t3, t4 being Element of (TermAlg S),(the_result_sort_of o) st t3 = # (t1,w) & t4 = # (t2,w) holds
A0 |= t3 '=' t4
let A0 be X0,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for w being ManySortedFunction of X0, the carrier of S --> NAT
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X0)))
for q being Element of Args (o,A0) st (canonical_homomorphism A0) # p = q holds
for t1, t2 being Term of S,X0 st t1 = (Den (o,(Free (S,X0)))) . p & t2 = (Den (o,A0)) . q holds
for t3, t4 being Element of (TermAlg S),(the_result_sort_of o) st t3 = # (t1,w) & t4 = # (t2,w) holds
A0 |= t3 '=' t4
set A = A0;
let w be ManySortedFunction of X0, the carrier of S --> NAT; :: thesis: for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X0)))
for q being Element of Args (o,A0) st (canonical_homomorphism A0) # p = q holds
for t1, t2 being Term of S,X0 st t1 = (Den (o,(Free (S,X0)))) . p & t2 = (Den (o,A0)) . q holds
for t3, t4 being Element of (TermAlg S),(the_result_sort_of o) st t3 = # (t1,w) & t4 = # (t2,w) holds
A0 |= t3 '=' t4
set Y = the carrier of S --> NAT;
let o be OperSymbol of S; :: thesis: for p being Element of Args (o,(Free (S,X0)))
for q being Element of Args (o,A0) st (canonical_homomorphism A0) # p = q holds
for t1, t2 being Term of S,X0 st t1 = (Den (o,(Free (S,X0)))) . p & t2 = (Den (o,A0)) . q holds
for t3, t4 being Element of (TermAlg S),(the_result_sort_of o) st t3 = # (t1,w) & t4 = # (t2,w) holds
A0 |= t3 '=' t4
let p be Element of Args (o,(Free (S,X0))); :: thesis: for q being Element of Args (o,A0) st (canonical_homomorphism A0) # p = q holds
for t1, t2 being Term of S,X0 st t1 = (Den (o,(Free (S,X0)))) . p & t2 = (Den (o,A0)) . q holds
for t3, t4 being Element of (TermAlg S),(the_result_sort_of o) st t3 = # (t1,w) & t4 = # (t2,w) holds
A0 |= t3 '=' t4
let q be Element of Args (o,A0); :: thesis: ( (canonical_homomorphism A0) # p = q implies for t1, t2 being Term of S,X0 st t1 = (Den (o,(Free (S,X0)))) . p & t2 = (Den (o,A0)) . q holds
for t3, t4 being Element of (TermAlg S),(the_result_sort_of o) st t3 = # (t1,w) & t4 = # (t2,w) holds
A0 |= t3 '=' t4 )
assume A1: (canonical_homomorphism A0) # p = q ; :: thesis: for t1, t2 being Term of S,X0 st t1 = (Den (o,(Free (S,X0)))) . p & t2 = (Den (o,A0)) . q holds
for t3, t4 being Element of (TermAlg S),(the_result_sort_of o) st t3 = # (t1,w) & t4 = # (t2,w) holds
A0 |= t3 '=' t4
Free (S,X0) = FreeMSA X0 by MSAFREE3:31;
then reconsider p0 = p as ArgumentSeq of Sym (o,X0) by INSTALG1:1;
let t1, t2 be Term of S,X0; :: thesis: ( t1 = (Den (o,(Free (S,X0)))) . p & t2 = (Den (o,A0)) . q implies for t3, t4 being Element of (TermAlg S),(the_result_sort_of o) st t3 = # (t1,w) & t4 = # (t2,w) holds
A0 |= t3 '=' t4 )
assume A2: ( t1 = (Den (o,(Free (S,X0)))) . p & t2 = (Den (o,A0)) . q ) ; :: thesis: for t3, t4 being Element of (TermAlg S),(the_result_sort_of o) st t3 = # (t1,w) & t4 = # (t2,w) holds
A0 |= t3 '=' t4
let t3, t4 be Element of (TermAlg S),(the_result_sort_of o); :: thesis: ( t3 = # (t1,w) & t4 = # (t2,w) implies A0 |= t3 '=' t4 )
assume A3: ( t3 = # (t1,w) & t4 = # (t2,w) ) ; :: thesis: A0 |= t3 '=' t4
reconsider t1 = t1 as Element of (Free (S,X0)),(the_result_sort_of o) by A2, MSUALG_9:18;
t2 = ((canonical_homomorphism A0) . (the_result_sort_of o)) . t1 by A1, A2, Def10, MSUALG_3:def 7;
hence A0 |= t3 '=' t4 by A3, Th71; :: thesis: verum