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 ; :: thesis: ( B is vf-free & B is integer-array )
thus B is vf-free by A1; :: thesis: 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 ; :: according to AOFA_A01:def 14 :: thesis: 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; :: thesis: verum