let I be set ; :: thesis: for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B st F is "onto" holds
F .:.: A = B
let A, B be ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B st F is "onto" holds
F .:.: A = B
let F be ManySortedFunction of A,B; :: thesis: ( F is "onto" implies F .:.: A = B )
assume A1: F is "onto" ; :: thesis: F .:.: A = B

now

let i be set ; :: thesis: ( i in I implies (F .:.: A) . b₁ = B . b₁ )
assume A2: i in I ; :: thesis: (F .:.: A) . b₁ = B . b₁
then A3: F . i is Function of (A . i),(B . i) by PBOOLE:def 15;

per cases not ( B . i = {} & not A . i = {} & not ( B . i = {} & not A . i = {} ) ) ;

suppose A4: ( B . i = {} implies A . i = {} ) ; :: thesis: (F .:.: A) . b₁ = B . b₁

thus (F .:.: A) . i = (F . i) .: (A . i) by A2, PBOOLE:def 20
.= rng (F . i) by A3, A4, FUNCT_2:37
.= B . i by A1, A2, MSUALG_3:def 3 ; :: thesis: verum

end;

suppose A5: ( B . i = {} & not A . i = {} ) ; :: thesis: (F .:.: A) . b₁ = B . b₁

then A6: F . i = {} by A3;
thus (F .:.: A) . i = (F . i) .: (A . i) by A2, PBOOLE:def 20
.= B . i by A5, A6, RELAT_1:117 ; :: thesis: verum

end;

end;

end;

hence F .:.: A = B by PBOOLE:3; :: thesis: verum