let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra over S

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds

F is ManySortedFunction of U1,(Image F)

let U1, U2 be non-empty MSAlgebra over S; :: thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds

F is ManySortedFunction of U1,(Image F)

let F be ManySortedFunction of U1,U2; :: thesis: ( F is_homomorphism U1,U2 implies F is ManySortedFunction of U1,(Image F) )

assume A1: F is_homomorphism U1,U2 ; :: thesis: F is ManySortedFunction of U1,(Image F)

for i being object st i in the carrier of S holds

F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i)

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds

F is ManySortedFunction of U1,(Image F)

let U1, U2 be non-empty MSAlgebra over S; :: thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds

F is ManySortedFunction of U1,(Image F)

let F be ManySortedFunction of U1,U2; :: thesis: ( F is_homomorphism U1,U2 implies F is ManySortedFunction of U1,(Image F) )

assume A1: F is_homomorphism U1,U2 ; :: thesis: F is ManySortedFunction of U1,(Image F)

for i being object st i in the carrier of S holds

F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i)

proof

hence
F is ManySortedFunction of U1,(Image F)
by PBOOLE:def 15; :: thesis: verum
let i be object ; :: thesis: ( i in the carrier of S implies F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i) )

assume A2: i in the carrier of S ; :: thesis: F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i)

then reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def 15;

A3: dom f = the Sorts of U1 . i by A2, FUNCT_2:def 1;

the Sorts of (Image F) = F .:.: the Sorts of U1 by A1, Def12;

then the Sorts of (Image F) . i = f .: ( the Sorts of U1 . i) by A2, PBOOLE:def 20

.= rng f by A3, RELAT_1:113 ;

hence F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i) by A3, FUNCT_2:1; :: thesis: verum

end;assume A2: i in the carrier of S ; :: thesis: F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i)

then reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def 15;

A3: dom f = the Sorts of U1 . i by A2, FUNCT_2:def 1;

the Sorts of (Image F) = F .:.: the Sorts of U1 by A1, Def12;

then the Sorts of (Image F) . i = f .: ( the Sorts of U1 . i) by A2, PBOOLE:def 20

.= rng f by A3, RELAT_1:113 ;

hence F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i) by A3, FUNCT_2:1; :: thesis: verum