let I be non empty set ; :: thesis: for A being ManySortedSet of I holds
( 2 c= card (product A) iff ( A is non-empty & not A is trivial-yielding ) )
let A be ManySortedSet of I; :: thesis: ( 2 c= card (product A) iff ( A is non-empty & not A is trivial-yielding ) )
A1: dom A = I by PARTFUN1:def 2;
thus ( 2 c= card (product A) implies ( A is non-empty & not A is trivial-yielding ) ) :: thesis: ( A is non-empty & not A is trivial-yielding implies 2 c= card (product A) )

proof

assume 2 c= card (product A) ; :: thesis: ( A is non-empty & not A is trivial-yielding )
then consider a, b being object such that
A2: a in product A and
A3: b in product A and
A4: a <> b by Th2;
consider a1 being Function such that
A5: ( a = a1 & dom a1 = dom A ) and
A6: for e being object st e in dom A holds
a1 . e in A . e by A2, CARD_3:def 5;
thus A is non-empty by A1, A6; :: thesis: not A is trivial-yielding
consider b1 being Function such that
A7: ( b = b1 & dom b1 = dom A ) and
A8: for e being object st e in dom A holds
b1 . e in A . e by A3, CARD_3:def 5;
consider e being object such that
A9: e in dom A and
A10: b1 . e <> a1 . e by A4, A5, A7, FUNCT_1:2;
thus not A is trivial-yielding :: thesis: verum

proof

take A . e ; :: according to PENCIL_1:def 16 :: thesis: ( A . e in rng A & not A . e is trivial )
thus A . e in rng A by A9, FUNCT_1:def 3; :: thesis: not A . e is trivial
( a1 . e in A . e & b1 . e in A . e ) by A6, A8, A9;
then 2 c= card (A . e) by A10, Th2;
hence not A . e is trivial by Th4; :: thesis: verum

end;

end;

assume A11: ( A is non-empty & not A is trivial-yielding ) ; :: thesis: 2 c= card (product A)
then consider r being set such that
A12: r in rng A and
A13: not r is trivial ;

now :: thesis: not {} in rng A

assume {} in rng A ; :: thesis: contradiction
then ex o being object st
( o in dom A & A . o = {} ) by FUNCT_1:def 3;
hence contradiction by A1, A11; :: thesis: verum

end;

then not product A is empty by CARD_3:26;
then consider a1 being object such that
A14: a1 in product A ;
consider p being object such that
A15: p in dom A and
A16: r = A . p by A12, FUNCT_1:def 3;
consider a being Function such that
A17: a = a1 and
A18: dom a = dom A and
A19: for o being object st o in dom A holds
a . o in A . o by A14, CARD_3:def 5;
reconsider a = a as ManySortedSet of I by A1, A18, PARTFUN1:def 2, RELAT_1:def 18;
2 c= card r by A13, Th4;
then consider t being object such that
A20: t in r and
A21: t <> a . p by Th3;
reconsider p = p as Element of I by A15, PARTFUN1:def 2;
set b = a +* (p,t);

A22: now :: thesis: for o being object st o in dom A holds
(a +* (p,t)) . o in A . o

let o be object ; :: thesis: ( o in dom A implies (a +* (p,t)) . b₁ in A . b₁ )
assume A23: o in dom A ; :: thesis: (a +* (p,t)) . b₁ in A . b₁

per cases ( o <> p or o = p ) ;

suppose o <> p ; :: thesis: (a +* (p,t)) . b₁ in A . b₁

then (a +* (p,t)) . o = a . o by FUNCT_7:32;
hence (a +* (p,t)) . o in A . o by A19, A23; :: thesis: verum

end;

suppose o = p ; :: thesis: (a +* (p,t)) . b₁ in A . b₁

hence (a +* (p,t)) . o in A . o by A18, A15, A16, A20, FUNCT_7:31; :: thesis: verum

end;

end;

end;

dom (a +* (p,t)) = I by PARTFUN1:def 2
.= dom A by PARTFUN1:def 2 ;
then A24: a +* (p,t) in product A by A22, CARD_3:9;
(a +* (p,t)) . p = t by A18, A15, FUNCT_7:31;
hence 2 c= card (product A) by A14, A17, A21, A24, Th2; :: thesis: verum