defpred S1[ object , object ] means P1[$1,$2 `1 ,$2 `2 ];
deffunc H1( object ) -> set = [:(F2() . $1),(F2() . $1):];
consider R being Function such that
A1: dom R = F1() and
A2: for i being object st i in F1() holds
for a being object holds
( a in R . i iff ( a in H1(i) & S1[i,a] ) ) from CARD_3:sch 2();
 reconsider R = R as ManySortedSet of F1() by A1, PARTFUN1:def 2, RELAT_1:def 18;
R is ManySortedRelation of F2()
proof
let i be set ; :: according to MSUALG_4:def 1 :: thesis: ( not i in F1() or R . i is Element of bool [:(F2() . i),(F2() . i):] )
assume A3: i in F1() ; :: thesis: R . i is Element of bool [:(F2() . i),(F2() . i):]
R . i c= [:(F2() . i),(F2() . i):] by A2, A3;
hence R . i is Element of bool [:(F2() . i),(F2() . i):] ; :: thesis: verum
end;
then reconsider R = R as ManySortedRelation of F2() ;
take R ; :: thesis: for i being Element of F1()
for a, b being Element of F2() . i holds
( [a,b] in R . i iff P1[i,a,b] )
let i be Element of F1(); :: thesis: for a, b being Element of F2() . i holds
( [a,b] in R . i iff P1[i,a,b] )
let a, b be Element of F2() . i; :: thesis: ( [a,b] in R . i iff P1[i,a,b] )
A4: [a,b] `2 = b ;
A5: [a,b] in [:(F2() . i),(F2() . i):] by ZFMISC_1:87;
[a,b] `1 = a ;
hence ( [a,b] in R . i iff P1[i,a,b] ) by A2, A4, A5; :: thesis: verum