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 G being basic GeneratorSystem over S,X,T
for s being Element of C -States the generators of G
for h being ManySortedFunction of T,C st h is_homomorphism T,C & s = h || the generators of G holds
for a being SortSymbol of S
for t being Element of T,a holds t value_at (C,s) = (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 G being basic GeneratorSystem over S,X,T
for s being Element of C -States the generators of G
for h being ManySortedFunction of T,C st h is_homomorphism T,C & s = h || the generators of G holds
for a being SortSymbol of S
for t being Element of T,a holds t value_at (C,s) = (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 G being basic GeneratorSystem over S,X,T
for s being Element of C -States the generators of G
for h being ManySortedFunction of T,C st h is_homomorphism T,C & s = h || the generators of G holds
for a being SortSymbol of S
for t being Element of T,a holds t value_at (C,s) = (h . a) . t
let C be bool-correct 4,1 integer image of T; :: thesis: for G being basic GeneratorSystem over S,X,T
for s being Element of C -States the generators of G
for h being ManySortedFunction of T,C st h is_homomorphism T,C & s = h || the generators of G holds
for a being SortSymbol of S
for t being Element of T,a holds t value_at (C,s) = (h . a) . t
let G be basic GeneratorSystem over S,X,T; :: thesis: for s being Element of C -States the generators of G
for h being ManySortedFunction of T,C st h is_homomorphism T,C & s = h || the generators of G holds
for a being SortSymbol of S
for t being Element of T,a holds t value_at (C,s) = (h . a) . t
let s be Element of C -States the generators of G; :: thesis: for h being ManySortedFunction of T,C st h is_homomorphism T,C & s = h || the generators of G holds
for a being SortSymbol of S
for t being Element of T,a holds t value_at (C,s) = (h . a) . t
let h be ManySortedFunction of T,C; :: thesis: ( h is_homomorphism T,C & s = h || the generators of G implies for a being SortSymbol of S
for t being Element of T,a holds t value_at (C,s) = (h . a) . t )
assume A1: h is_homomorphism T,C ; :: thesis: ( not s = h || the generators of G or for a being SortSymbol of S
for t being Element of T,a holds t value_at (C,s) = (h . a) . t )
assume A2: s = h || the generators of G ; :: thesis: for a being SortSymbol of S
for t being Element of T,a holds t value_at (C,s) = (h . a) . t
let a be SortSymbol of S; :: thesis: for t being Element of T,a holds t value_at (C,s) = (h . a) . t
let t be Element of T,a; :: thesis: t value_at (C,s) = (h . a) . t
A3: s is ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
the generators of G is_transformable_to the Sorts of C by MSAFREE4:21;
then A4: doms s = the generators of G by A3, MSSUBFAM:17;
thus t value_at (C,s) = (h . a) . t by A4, A1, A2, AOFA_A00:def 21; :: thesis: verum