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 "" is "1-1" & F "" is "onto" )

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 "" is "1-1" & F "" is "onto" )

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

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

thus F "" is "onto" :: thesis: verum

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

( F "" is "1-1" & F "" is "onto" )

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 "" is "1-1" & F "" is "onto" )

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

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

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

(F "") . i is one-to-one

hence
F "" is "1-1"
by MSUALG_3:1; :: thesis: F "" is "onto" (F "") . i is one-to-one

let i be set ; :: thesis: ( i in I implies (F "") . i is one-to-one )

assume A2: i in I ; :: thesis: (F "") . i is one-to-one

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

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

then g " is one-to-one ;

hence (F "") . i is one-to-one by A1, A2, MSUALG_3:def 4; :: thesis: verum

end;assume A2: i in I ; :: thesis: (F "") . i is one-to-one

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

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

then g " is one-to-one ;

hence (F "") . i is one-to-one by A1, A2, MSUALG_3:def 4; :: thesis: verum

thus F "" is "onto" :: thesis: verum

proof

let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in I or rng ((F "") . i) = A . i )

assume A3: i in I ; :: thesis: rng ((F "") . i) = A . i

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

A4: g is one-to-one by A1, A3, MSUALG_3:1;

A . i = dom g by A3, FUNCT_2:def 1

.= rng (g ") by A4, FUNCT_1:33 ;

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

end;assume A3: i in I ; :: thesis: rng ((F "") . i) = A . i

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

A4: g is one-to-one by A1, A3, MSUALG_3:1;

A . i = dom g by A3, FUNCT_2:def 1

.= rng (g ") by A4, FUNCT_1:33 ;

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