let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of S
for T being non-empty b₁,S -terms free_in_itself MSAlgebra over S
for A being image of T
for G being GeneratorSet of T st G = FreeGen X holds
for f being ManySortedFunction of G, the Sorts of A ex h being ManySortedFunction of T,A st
( h is_homomorphism T,A & f = h || G )
let X be non-empty ManySortedSet of S; :: thesis: for T being non-empty X,S -terms free_in_itself MSAlgebra over S
for A being image of T
for G being GeneratorSet of T st G = FreeGen X holds
for f being ManySortedFunction of G, the Sorts of A ex h being ManySortedFunction of T,A st
( h is_homomorphism T,A & f = h || G )
let T be non-empty X,S -terms free_in_itself MSAlgebra over S; :: thesis: for A being image of T
for G being GeneratorSet of T st G = FreeGen X holds
for f being ManySortedFunction of G, the Sorts of A ex h being ManySortedFunction of T,A st
( h is_homomorphism T,A & f = h || G )
let A be image of T; :: thesis: for G being GeneratorSet of T st G = FreeGen X holds
for f being ManySortedFunction of G, the Sorts of A ex h being ManySortedFunction of T,A st
( h is_homomorphism T,A & f = h || G )
let G be GeneratorSet of T; :: thesis: ( G = FreeGen X implies for f being ManySortedFunction of G, the Sorts of A ex h being ManySortedFunction of T,A st
( h is_homomorphism T,A & f = h || G ) )
assume A1: G = FreeGen X ; :: thesis: for f being ManySortedFunction of G, the Sorts of A ex h being ManySortedFunction of T,A st
( h is_homomorphism T,A & f = h || G )
let f be ManySortedFunction of G, the Sorts of A; :: thesis: ex h being ManySortedFunction of T,A st
( h is_homomorphism T,A & f = h || G )
reconsider H = FreeGen X as non-empty GeneratorSet of Free (S,X) by MSAFREE3:31;
consider j being ManySortedFunction of T,A such that
A2: j is_epimorphism T,A by Def5;
A3: ( j is_homomorphism T,A & j is "onto" ) by A2;
consider jj being ManySortedFunction of A,T such that
A4: j ** jj = id the Sorts of A by A3, Th23, Th21;
consider h being ManySortedFunction of T,T such that
A5: ( h is_homomorphism T,T & jj ** f = h || G ) by A1, Def9;
take k = j ** h; :: thesis: ( k is_homomorphism T,A & f = k || G )
thus k is_homomorphism T,A by A3, A5, MSUALG_3:10; :: thesis: f = k || G
thus f = (id the Sorts of A) ** f by MSUALG_3:4
.= j ** (jj ** f) by A4, PBOOLE:140
.= k || G by A5, EXTENS_1:4 ; :: thesis: verum