let F be non-empty MSAlgebra over S; ( F = Free (S,X) implies F is integer-array )
assume A1:
F = Free (S,X)
; 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
; AOFA_A01:def 14 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
; verum