hereby :: thesis: ( not I2 <> {} implies ex b1 being ManySortedSet of st b1 = [0] I1 )
assume
I2 <> {}
;
:: thesis: ex IT' being ManySortedSet of ex I2' being non empty set ex B' being ManySortedSet of ex f' being Function of I1,I2' st
( f = f' & B = B' & IT' is ManySortedFunction of A,B' * f' )then reconsider I2' =
I2 as non
empty set ;
reconsider f' =
f as
Function of
I1,
I2' ;
reconsider B' =
B as
ManySortedSet of ;
consider IT being
ManySortedFunction of
A,
B' * f';
reconsider IT' =
IT as
ManySortedSet of ;
take IT' =
IT';
:: thesis: ex I2' being non empty set ex B' being ManySortedSet of ex f' being Function of I1,I2' st
( f = f' & B = B' & IT' is ManySortedFunction of A,B' * f' )take I2' =
I2';
:: thesis: ex B' being ManySortedSet of ex f' being Function of I1,I2' st
( f = f' & B = B' & IT' is ManySortedFunction of A,B' * f' )reconsider f' =
f as
Function of
I1,
I2' ;
reconsider B' =
B as
ManySortedSet of ;
take B' =
B';
:: thesis: ex f' being Function of I1,I2' st
( f = f' & B = B' & IT' is ManySortedFunction of A,B' * f' )take f' =
f';
:: thesis: ( f = f' & B = B' & IT' is ManySortedFunction of A,B' * f' )thus
(
f = f' &
B = B' )
;
:: thesis: IT' is ManySortedFunction of A,B' * f'thus
IT' is
ManySortedFunction of
A,
B' * f'
;
:: thesis: verum
end;
thus
( not I2 <> {} implies ex b1 being ManySortedSet of st b1 = [0] I1 )
; :: thesis: verum