let I be non empty set ; :: thesis: for A being ManySortedSet of holds
( 2 c= card (product A) iff ( A is non-empty & not A is trivial-yielding ) )
let A be ManySortedSet of ; :: thesis: ( 2 c= card (product A) iff ( A is non-empty & not A is trivial-yielding ) )
A1: dom A = I by PARTFUN1:def 4;
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 set such that
A2: ( a in product A & b in product A & a <> b ) by Th2;
consider a1 being Function such that
A3: ( a = a1 & dom a1 = dom A & ( for e being set st e in dom A holds
a1 . e in A . e ) ) by A2, CARD_3:def 5;
consider b1 being Function such that
A4: ( b = b1 & dom b1 = dom A & ( for e being set st e in dom A holds
b1 . e in A . e ) ) by A2, CARD_3:def 5;
consider e being set such that
A5: ( e in dom A & b1 . e <> a1 . e ) by A2, A3, A4, FUNCT_1:9;
thus A is non-empty :: thesis: not A is trivial-yielding

proof

let i be set ; :: according to PBOOLE:def 16 :: thesis: ( not i in I or not A . i is empty )
assume i in I ; :: thesis: not A . i is empty
hence not A . i is empty by A1, A3; :: thesis: verum

end;

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 A5, FUNCT_1:def 5; :: thesis: not A . e is trivial
( a1 . e in A . e & b1 . e in A . e ) by A3, A4, A5;
then 2 c= card (A . e) by A5, Th2;
hence not A . e is trivial by Th4; :: thesis: verum

end;

end;

assume A6: ( A is non-empty & not A is trivial-yielding ) ; :: thesis: 2 c= card (product A)

now

assume {} in rng A ; :: thesis: contradiction
then consider o being set such that
A7: ( o in dom A & A . o = {} ) by FUNCT_1:def 5;
thus contradiction by A1, A6, A7, PBOOLE:def 16; :: thesis: verum

end;

then not product A is empty by CARD_3:37;
then consider a1 being set such that
A8: a1 in product A by XBOOLE_0:def 1;
consider a being Function such that
A9: ( a = a1 & dom a = dom A & ( for o being set st o in dom A holds
a . o in A . o ) ) by A8, CARD_3:def 5;
reconsider a = a as ManySortedSet of by A1, A9, PARTFUN1:def 4, RELAT_1:def 18;
consider r being set such that
A10: ( r in rng A & not r is trivial ) by A6, Def16;
consider p being set such that
A11: ( p in dom A & r = A . p ) by A10, FUNCT_1:def 5;
2 c= card r by A10, Th4;
then consider t being set such that
A12: ( t in r & t <> a . p ) by Th3;
reconsider p = p as Element of I by A11, PARTFUN1:def 4;
set b = a +* p,t;
A13: (a +* p,t) . p = t by A9, A11, FUNCT_7:33;
A14: dom (a +* p,t) = I by PARTFUN1:def 4
.= dom A by PARTFUN1:def 4 ;

now

let o be set ; :: thesis: ( o in dom A implies (a +* p,t) . b₁ in A . b₁ )
assume A15: 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:34;
hence (a +* p,t) . o in A . o by A9, A15; :: thesis: verum

end;

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

hence (a +* p,t) . o in A . o by A9, A11, A12, FUNCT_7:33; :: thesis: verum

end;

end;

end;

then a +* p,t in product A by A14, CARD_3:18;
hence 2 c= card (product A) by A8, A9, A12, A13, Th2; :: thesis: verum