let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for X being non-empty 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 a being SortSymbol of S
for x being Element of the generators of G . a holds (@ x) value_at (C,s) = (s . a) . x
let X be non-empty 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 a being SortSymbol of S
for x being Element of the generators of G . a holds (@ x) value_at (C,s) = (s . a) . x
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 a being SortSymbol of S
for x being Element of the generators of G . a holds (@ x) value_at (C,s) = (s . a) . x
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 a being SortSymbol of S
for x being Element of the generators of G . a holds (@ x) value_at (C,s) = (s . a) . x
let G be basic GeneratorSystem over S,X,T; :: thesis: for s being Element of C -States the generators of G
for a being SortSymbol of S
for x being Element of the generators of G . a holds (@ x) value_at (C,s) = (s . a) . x
let s be Element of C -States the generators of G; :: thesis: for a being SortSymbol of S
for x being Element of the generators of G . a holds (@ x) value_at (C,s) = (s . a) . x
let a be SortSymbol of S; :: thesis: for x being Element of the generators of G . a holds (@ x) value_at (C,s) = (s . a) . x
let x be Element of the generators of G . a; :: thesis: (@ x) value_at (C,s) = (s . a) . x
s is ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
then consider h being ManySortedFunction of T,C such that
A1: ( h is_homomorphism T,C & s = h || the generators of G ) by AOFA_A00:def 19;
(@ x) value_at (C,s) = (h . a) . x by A1, Th29
.= ((h . a) | ( the generators of G . a)) . x by FUNCT_1:49 ;
hence (@ x) value_at (C,s) = (s . a) . x by A1, MSAFREE:def 1; :: thesis: verum