let I be set ; :: thesis: for A, B being non-empty ManySortedSet of I
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 non-empty ManySortedSet of I; :: 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 that
A1: F is "1-1" and
A2: F is "onto" and
A3: G ** F = id A ; :: thesis: G = F ""

now :: thesis: for i being object st i in I holds
G . i = (F "") . i

let i be object ; :: thesis: ( i in I implies G . i = (F "") . i )
assume A4: i in I ; :: thesis: G . i = (F "") . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
A5: f is one-to-one by A1, A4, MSUALG_3:1;
reconsider g = G . i as Function of (B . i),(A . i) by A4, PBOOLE:def 15;
(G ** F) . i = id (A . i) by A3, A4, MSUALG_3:def 1;
then A6: g * f = id (A . i) by A4, MSUALG_3:2;
( (F "") . i = f " & rng f = B . i ) by A1, A2, A4, MSUALG_3:def 4;
hence G . i = (F "") . i by A4, A6, A5, FUNCT_2:30; :: thesis: verum

end;

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