let J be non empty set ; :: thesis: for A, B being set
for f being Function of A,B
for g being Function of B,A st g * f = id A holds
(J => g) ** (J => f) = id (J --> A)
let A, B be set ; :: thesis: for f being Function of A,B
for g being Function of B,A st g * f = id A holds
(J => g) ** (J => f) = id (J --> A)
let f be Function of A,B; :: thesis: for g being Function of B,A st g * f = id A holds
(J => g) ** (J => f) = id (J --> A)
let g be Function of B,A; :: thesis: ( g * f = id A implies (J => g) ** (J => f) = id (J --> A) )
set F = (J => g) ** (J => f);
dom ((J => g) ** (J => f)) = J by MSUALG_3:2;
then reconsider F = (J => g) ** (J => f) as ManySortedSet of J by PARTFUN1:def 2, RELAT_1:def 18;
assume A1: g * f = id A ; :: thesis: (J => g) ** (J => f) = id (J --> A)
A2: for j being object st j in J holds
F . j = id ((J --> A) . j)

proof

let j be object ; :: thesis: ( j in J implies F . j = id ((J --> A) . j) )
assume A3: j in J ; :: thesis: F . j = id ((J --> A) . j)
then A4: (J --> A) . j = A by FUNCOP_1:7;
( (J => g) . j = g & (J => f) . j = f ) by A3, FUNCOP_1:7;
hence F . j = id ((J --> A) . j) by A1, A3, A4, MSUALG_3:2; :: thesis: verum

end;

now :: thesis: for j being object st j in J holds
F . j is Function of ((J --> A) . j),((J --> A) . j)

let j be object ; :: thesis: ( j in J implies F . j is Function of ((J --> A) . j),((J --> A) . j) )
assume j in J ; :: thesis: F . j is Function of ((J --> A) . j),((J --> A) . j)
then F . j = id ((J --> A) . j) by A2;
hence F . j is Function of ((J --> A) . j),((J --> A) . j) ; :: thesis: verum

end;

then reconsider F = F as ManySortedFunction of J --> A,J --> A by PBOOLE:def 15;
for j being set st j in J holds
F . j = id ((J --> A) . j) by A2;
hence (J => g) ** (J => f) = id (J --> A) by MSUALG_3:def 1; :: thesis: verum