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 :: thesis: for i being object st i in I holds
(F .:.: A) . i = B . i

let i be object ; :: 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 ( 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, RELSET_1:22
.= B . i by A1, A2 ; :: thesis: verum

end;

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

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

end;

end;

end;

hence F .:.: A = B ; :: thesis: verum