let I be set ; :: thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds
for f being ManySortedFunction of A,B st f is "onto" holds
ex g being ManySortedFunction of B,A st f ** g = id B
let A, B be ManySortedSet of I; :: thesis: ( A is_transformable_to B implies for f being ManySortedFunction of A,B st f is "onto" holds
ex g being ManySortedFunction of B,A st f ** g = id B )
assume A1: A is_transformable_to B ; :: thesis: for f being ManySortedFunction of A,B st f is "onto" holds
ex g being ManySortedFunction of B,A st f ** g = id B
let f be ManySortedFunction of A,B; :: thesis: ( f is "onto" implies ex g being ManySortedFunction of B,A st f ** g = id B )
assume A2: f is "onto" ; :: thesis: ex g being ManySortedFunction of B,A st f ** g = id B
deffunc H₂( object ) -> rng-retract of f . $1 = the rng-retract of f . $1;
consider g being ManySortedSet of I such that
A3: for i being object st i in I holds
g . i = H₂(i) from PBOOLE:sch 4();
g is Function-yielding

proof

let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 g or g . x is set )
assume x in dom g ; :: thesis: g . x is set
then g . x = H₂(x) by A3;
hence g . x is set ; :: thesis: verum

end;

then reconsider g = g as ManySortedFunction of I ;
g is ManySortedFunction of B,A

proof

let x be object ; :: according to PBOOLE:def 15 :: thesis: ( not x in I or g . x is Element of bool [:(B . x),(A . x):] )
assume A4: x in I ; :: thesis: g . x is Element of bool [:(B . x),(A . x):]
then A5: g . x = H₂(x) by A3;
then A6: ( dom (g . x) = rng (f . x) & rng (f . x) = B . x ) by A2, A4, ALGSPEC1:def 2;
( A . x <> {} implies B . x <> {} ) by A4, A1, PZFMISC1:def 3;
then A7: dom (f . x) = A . x by FUNCT_2:def 1;
A8: ( (f . x) * (g . x) = id (B . x) & dom (id (B . x)) = B . x ) by A5, A6, ALGSPEC1:def 2;
rng (g . x) c= dom (f . x)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (g . x) or y in dom (f . x) )
assume y in rng (g . x) ; :: thesis: y in dom (f . x)
then consider z being object such that
A9: ( z in dom (g . x) & y = (g . x) . z ) by FUNCT_1:def 3;
thus y in dom (f . x) by A6, A8, A9, FUNCT_1:11; :: thesis: verum

end;

hence g . x is Element of bool [:(B . x),(A . x):] by A6, A7, FUNCT_2:2; :: thesis: verum

end;

then reconsider g = g as ManySortedFunction of B,A ;
take g ; :: thesis: f ** g = id B

now :: thesis: for x being object st x in I holds
(f ** g) . x = (id B) . x

let x be object ; :: thesis: ( x in I implies (f ** g) . x = (id B) . x )
assume A10: x in I ; :: thesis: (f ** g) . x = (id B) . x
then g . x = H₂(x) by A3;
then ( (f . x) * (g . x) = id (rng (f . x)) & dom (g . x) = rng (f . x) & rng (f . x) = B . x ) by A2, A10, ALGSPEC1:def 2;
hence (f ** g) . x = id (B . x) by A10, MSUALG_3:2
.= (id B) . x by A10, MSUALG_3:def 1 ;
:: thesis: verum

end;

hence f ** g = id B ; :: thesis: verum