let I be set ; 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; 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; 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; ( 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
; G = F ""
now for i being object st i in I holds
G . i = (F "") . ilet i be
object ;
( i in I implies G . i = (F "") . i )assume A4:
i in I
;
G . i = (F "") . ithen 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;
verum end;
hence
G = F ""
by PBOOLE:3; verum