let I be set ; :: thesis: for A, B being V2() ManySortedSet of I

for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds

(F "") "" = F

let A, B be V2() ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds

(F "") "" = F

let F be ManySortedFunction of A,B; :: thesis: ( F is "1-1" & F is "onto" implies (F "") "" = F )

assume A1: ( F is "1-1" & F is "onto" ) ; :: thesis: (F "") "" = F

for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds

(F "") "" = F

let A, B be V2() ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds

(F "") "" = F

let F be ManySortedFunction of A,B; :: thesis: ( F is "1-1" & F is "onto" implies (F "") "" = F )

assume A1: ( F is "1-1" & F is "onto" ) ; :: thesis: (F "") "" = F

now :: thesis: for i being object st i in I holds

((F "") "") . i = F . i

hence
(F "") "" = F
by PBOOLE:3; :: thesis: verum((F "") "") . i = F . i

let i be object ; :: thesis: ( i in I implies ((F "") "") . i = F . i )

assume A2: i in I ; :: thesis: ((F "") "") . i = F . i

then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;

reconsider f9 = (F "") . i as Function of (B . i),(A . i) by A2, PBOOLE:def 15;

f is one-to-one by A1, A2, MSUALG_3:1;

then A3: (f ") " = f by FUNCT_1:43;

( F "" is "1-1" & F "" is "onto" ) by A1, Th12;

then ((F "") "") . i = f9 " by A2, MSUALG_3:def 4;

hence ((F "") "") . i = F . i by A1, A2, A3, MSUALG_3:def 4; :: thesis: verum

end;assume A2: i in I ; :: thesis: ((F "") "") . i = F . i

then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;

reconsider f9 = (F "") . i as Function of (B . i),(A . i) by A2, PBOOLE:def 15;

f is one-to-one by A1, A2, MSUALG_3:1;

then A3: (f ") " = f by FUNCT_1:43;

( F "" is "1-1" & F "" is "onto" ) by A1, Th12;

then ((F "") "") . i = f9 " by A2, MSUALG_3:def 4;

hence ((F "") "") . i = F . i by A1, A2, A3, MSUALG_3:def 4; :: thesis: verum