hereby ( not I2 <> {} implies ex b1 being ManySortedSet of I1 st b1 = EmptyMS I1 )
assume
I2 <> {}
;
ex IT9 being ManySortedSet of I1 ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 )then reconsider I29 =
I2 as non
empty set ;
reconsider f9 =
f as
Function of
I1,
I29 ;
reconsider B9 =
B as
ManySortedSet of
I29 ;
set IT = the
ManySortedFunction of
A,
B9 * f9;
reconsider IT9 = the
ManySortedFunction of
A,
B9 * f9 as
ManySortedSet of
I1 ;
take IT9 =
IT9;
ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 )take I29 =
I29;
ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 )reconsider f9 =
f as
Function of
I1,
I29 ;
reconsider B9 =
B as
ManySortedSet of
I29 ;
take B9 =
B9;
ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 )take f9 =
f9;
( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 )thus
(
f = f9 &
B = B9 )
;
IT9 is ManySortedFunction of A,B9 * f9thus
IT9 is
ManySortedFunction of
A,
B9 * f9
;
verum
end;
thus
( not I2 <> {} implies ex b1 being ManySortedSet of I1 st b1 = EmptyMS I1 )
; verum