set A = Free (S,X);
consider V being ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X)), B being X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S such that
A1:
( B = VarMSAlgebra(# the Sorts of (Free (S,X)), the Charact of (Free (S,X)),V #) & B is vf-free )
by AOFA_A00:39;
reconsider B = B as X,S -terms all_vars_including inheriting_operations free_in_itself strict VarMSAlgebra over S by A1;
take
B
; ( B is vf-free & B is integer-array )
thus
B is vf-free
by A1; B is integer-array
consider C being image of Free (S,X) such that
A2:
C is bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S
by Def14;
consider h being ManySortedFunction of (Free (S,X)),C such that
A3:
h is_epimorphism Free (S,X),C
by MSAFREE4:def 5;
reconsider g = h as ManySortedFunction of B,C by A1;
MSAlgebra(# the Sorts of C, the Charact of C #) = MSAlgebra(# the Sorts of C, the Charact of C #)
;
then reconsider D = C as image of B by A1, A3, Th8, MSAFREE4:def 5;
take
D
; AOFA_A01:def 14 D is bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S
thus
D is bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S
by A2; verum