hereby :: thesis: ( not I2 <> {} implies ex b₁ being ManySortedSet of I1 st b₁ = EmptyMS I1 )

assume I2 <> {} ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 )
take f9 = f9; :: thesis: ( f = f9 & B = B9 & IT9 is ManySortedFunction of A,B9 * f9 )
thus ( f = f9 & B = B9 ) ; :: thesis: IT9 is ManySortedFunction of A,B9 * f9
thus IT9 is ManySortedFunction of A,B9 * f9 ; :: thesis: verum

end;

thus ( not I2 <> {} implies ex b₁ being ManySortedSet of I1 st b₁ = EmptyMS I1 ) ; :: thesis: verum