let I be set ; :: thesis: for A being ManySortedSet of
for B, C being V2() ManySortedSet of
for f being ManySortedFunction of A,B
for g being ManySortedFunction of B,C st g ** f is "onto" holds
g is "onto"
let A be ManySortedSet of ; :: thesis: for B, C being V2() ManySortedSet of
for f being ManySortedFunction of A,B
for g being ManySortedFunction of B,C st g ** f is "onto" holds
g is "onto"
let B, C be V2() ManySortedSet of ; :: thesis: for f being ManySortedFunction of A,B
for g being ManySortedFunction of B,C st g ** f is "onto" holds
g is "onto"
let f be ManySortedFunction of A,B; :: thesis: for g being ManySortedFunction of B,C st g ** f is "onto" holds
g is "onto"
let g be ManySortedFunction of B,C; :: thesis: ( g ** f is "onto" implies g is "onto" )
assume A1: g ** f is "onto" ; :: thesis: g is "onto"
let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in I or rng (g . i) = C . i )
assume A2: i in I ; :: thesis: rng (g . i) = C . i
then A3: ( not B . i is empty & not C . i is empty ) ;
A4: ( f . i is Function of (A . i),(B . i) & g . i is Function of (B . i),(C . i) ) by A2, PBOOLE:def 18;
rng ((g . i) * (f . i)) = rng ((g ** f) . i) by A2, MSUALG_3:2
.= C . i by A1, A2, MSUALG_3:def 3 ;
hence rng (g . i) = C . i by A3, A4, Th1; :: thesis: verum