let I be set ; :: thesis: for A, B being V2() ManySortedSet of
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,A st F is "1-1" & F is "onto" & G ** F = id A holds
G = F ""
let A, B be V2() ManySortedSet of ; :: thesis: for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,A st F is "1-1" & F is "onto" & G ** F = id A holds
G = F ""
let F be ManySortedFunction of A,B; :: thesis: for G being ManySortedFunction of B,A st F is "1-1" & F is "onto" & G ** F = id A holds
G = F ""
let G be ManySortedFunction of B,A; :: thesis: ( F is "1-1" & F is "onto" & G ** F = id A implies G = F "" )
assume A1: ( F is "1-1" & F is "onto" & G ** F = id A ) ; :: thesis: G = F ""

now

let i be set ; :: thesis: ( i in I implies G . i = (F "" ) . i )
assume A2: i in I ; :: thesis: G . i = (F "" ) . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 18;
reconsider g = G . i as Function of (B . i),(A . i) by A2, PBOOLE:def 18;
A3: (F "" ) . i = f " by A1, A2, MSUALG_3:def 5;

now

thus A . i <> {} by A2; :: thesis: ( B . i <> {} & rng f = B . i & g * f = id (A . i) & f is one-to-one )
thus B . i <> {} by A2; :: thesis: ( rng f = B . i & g * f = id (A . i) & f is one-to-one )
thus rng f = B . i by A1, A2, MSUALG_3:def 3; :: thesis: ( g * f = id (A . i) & f is one-to-one )
(G ** F) . i = id (A . i) by A1, A2, MSUALG_3:def 1;
hence g * f = id (A . i) by A2, MSUALG_3:2; :: thesis: f is one-to-one
thus f is one-to-one by A1, A2, MSUALG_3:1; :: thesis: verum

end;

hence G . i = (F "" ) . i by A3, FUNCT_2:36; :: thesis: verum

end;

hence G = F "" by PBOOLE:3; :: thesis: verum