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 a being SortSymbol of S
for x being pure Element of the generators of G . a
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (@ x) value_at (C,u) = (u . a) . x
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 a being SortSymbol of S
for x being pure Element of the generators of G . a
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (@ x) value_at (C,u) = (u . 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 a being SortSymbol of S
for x being pure Element of the generators of G . a
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (@ x) value_at (C,u) = (u . a) . x
let C be bool-correct 4,1 integer image of T; :: thesis: for G being basic GeneratorSystem over S,X,T
for a being SortSymbol of S
for x being pure Element of the generators of G . a
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (@ x) value_at (C,u) = (u . a) . x
let G be basic GeneratorSystem over S,X,T; :: thesis: for a being SortSymbol of S
for x being pure Element of the generators of G . a
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (@ x) value_at (C,u) = (u . a) . x
let a be SortSymbol of S; :: thesis: for x being pure Element of the generators of G . a
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (@ x) value_at (C,u) = (u . a) . x
let x be pure Element of the generators of G . a; :: thesis: for u being ManySortedFunction of FreeGen T, the Sorts of C holds (@ x) value_at (C,u) = (u . a) . x
let u be ManySortedFunction of FreeGen T, the Sorts of C; :: thesis: (@ x) value_at (C,u) = (u . a) . x
consider h being ManySortedFunction of T,C such that
A1: ( h is_homomorphism T,C & u = h || (FreeGen T) ) by MSAFREE4:46;
FreeGen T is_transformable_to the Sorts of C by MSAFREE4:21;
then A2: doms u = FreeGen T by MSSUBFAM:17;
then consider f being ManySortedFunction of T,C, Q being GeneratorSet of T such that
A3: ( f is_homomorphism T,C & Q = doms u & u = f || Q & (@ x) value_at (C,u) = (f . a) . (@ x) ) by A1, AOFA_A00:def 21;
(@ x) value_at (C,u) = (h . a) . x by A1, A2, A3, EXTENS_1:19
.= ((h . a) | ((FreeGen T) . a)) . x by Def4, FUNCT_1:49 ;
hence (@ x) value_at (C,u) = (u . a) . x by A1, MSAFREE:def 1; :: thesis: verum