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)

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

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

now :: thesis: for j being object st j in J holds

F . j is Function of ((J --> A) . j),((J --> A) . j)

then reconsider F = F as ManySortedFunction of J --> A,J --> A by PBOOLE:def 15;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;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

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