assume 2 c= card (product A) ; :: thesis:
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 V2() by A1, A6; :: thesis:
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:

take A . e ; :: according to PENCIL_1:def 16 :: thesis:
thus A . e in rng A by A9, FUNCT_1:def 3; :: thesis:
( 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:

end;

assume A11: ( A is V2() & not A is trivial-yielding ) ; :: thesis:
then consider r being set such that
A12: r in rng A and
A13: not r is trivial ;

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);

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

end;

end;