let F be non-empty MSAlgebra over S; :: thesis: ( F = Free (S,X) implies F is integer-array )
assume A1: F = Free (S,X) ; :: thesis: F is integer-array
set A = the non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S;
reconsider G = FreeGen X as GeneratorSet of F by A1, MSAFREE3:31;
set f = the ManySortedFunction of G, the Sorts of the non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S;
( FreeGen X is free & F = FreeMSA X ) by A1, MSAFREE3:31;
then consider h being ManySortedFunction of F, the non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S such that
A2: ( h is_homomorphism F, the non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S & h || G = the ManySortedFunction of G, the Sorts of the non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S ) by MSAFREE:def 5;
reconsider C = Image h as image of F by A2, MSAFREE4:def 4;
take C ; :: according to AOFA_A01:def 14 :: thesis: C is bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S
thus C is bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S ; :: thesis: verum