let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for X being V3() ManySortedSet of the carrier of S
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for h being ManySortedFunction of T,C st h is_homomorphism T,C holds
for a being SortSymbol of S
for t being Element of T,a holds t value_at (C,(h || (FreeGen T))) = (h . a) . t
let X be V3() ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for h being ManySortedFunction of T,C st h is_homomorphism T,C holds
for a being SortSymbol of S
for t being Element of T,a holds t value_at (C,(h || (FreeGen T))) = (h . a) . t
let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S; :: thesis: for C being bool-correct 4,1 integer image of T
for h being ManySortedFunction of T,C st h is_homomorphism T,C holds
for a being SortSymbol of S
for t being Element of T,a holds t value_at (C,(h || (FreeGen T))) = (h . a) . t
let C be bool-correct 4,1 integer image of T; :: thesis: for h being ManySortedFunction of T,C st h is_homomorphism T,C holds
for a being SortSymbol of S
for t being Element of T,a holds t value_at (C,(h || (FreeGen T))) = (h . a) . t
let h be ManySortedFunction of T,C; :: thesis: ( h is_homomorphism T,C implies for a being SortSymbol of S
for t being Element of T,a holds t value_at (C,(h || (FreeGen T))) = (h . a) . t )
assume A1: h is_homomorphism T,C ; :: thesis: for a being SortSymbol of S
for t being Element of T,a holds t value_at (C,(h || (FreeGen T))) = (h . a) . t
set s = h || (FreeGen T);
let a be SortSymbol of S; :: thesis: for t being Element of T,a holds t value_at (C,(h || (FreeGen T))) = (h . a) . t
let t be Element of T,a; :: thesis: t value_at (C,(h || (FreeGen T))) = (h . a) . t
FreeGen T is_transformable_to the Sorts of C by MSAFREE4:21;
then A2: doms (h || (FreeGen T)) = FreeGen T by MSSUBFAM:17;
thus t value_at (C,(h || (FreeGen T))) = (h . a) . t by A2, A1, AOFA_A00:def 21; :: thesis: verum