now

let i be set ; :: thesis: ( i in I implies not [|A,B|] . i is empty )
assume A1: i in I ; :: thesis: not [|A,B|] . i is empty
then [|A,B|] . i = [:(A . i),(B . i):] by PBOOLE:def 16;
hence not [|A,B|] . i is empty by A1, ZFMISC_1:90; :: thesis: verum

end;

hence [|A,B|] is non-empty by PBOOLE:def 13; :: thesis: verum