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 ""

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

hence
G = F ""
by PBOOLE:3; :: thesis: verumG . 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;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