A1: now :: thesis: for i being Element of I holds J . i is Poset
let i be Element of I; :: thesis: J . i is Poset
dom J = I by PARTFUN1:def 2;
then J . i in rng J by FUNCT_1:def 3;
hence J . i is Poset by Def5; :: thesis: verum
end;
then for i being Element of I holds J . i is transitive ;
hence product J is transitive by WAYBEL_3:29; :: thesis: product J is antisymmetric
for i being Element of I holds J . i is antisymmetric by A1;
hence product J is antisymmetric by WAYBEL_3:30; :: thesis: verum