let I be set ; :: thesis: for A, B being V2() 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 V2() 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 ;
reconsider g = G . i as Function of (B . i),(A . i) by ;
(G ** F) . i = id (A . i) by ;
then A6: g * f = id (A . i) by ;
( (F "") . i = f " & rng f = B . i ) by ;
hence G . i = (F "") . i by ; :: thesis: verum
end;
hence G = F "" by PBOOLE:3; :: thesis: verum