defpred S₁[ object , object ] means P₁[$1,$2 `1 ,$2 `2 ];
deffunc H₁( object ) -> set = [:(F₂() . $1),(F₂() . $1):];
consider R being Function such that
A1: dom R = F₁() and
A2: for i being object st i in F₁() holds
for a being object holds
( a in R . i iff ( a in H₁(i) & S₁[i,a] ) ) from CARD_3:sch 2();
reconsider R = R as ManySortedSet of F₁() by A1, PARTFUN1:def 2, RELAT_1:def 18;
R is ManySortedRelation of F₂()

proof

let i be set ; :: according to MSUALG_4:def 1 :: thesis: ( not i in F₁() or R . i is Element of bool [:(F₂() . i),(F₂() . i):] )
assume A3: i in F₁() ; :: thesis: R . i is Element of bool [:(F₂() . i),(F₂() . i):]
R . i c= [:(F₂() . i),(F₂() . i):] by A2, A3;
hence R . i is Element of bool [:(F₂() . i),(F₂() . i):] ; :: thesis: verum

end;

then reconsider R = R as ManySortedRelation of F₂() ;
take R ; :: thesis: for i being Element of F₁()
for a, b being Element of F₂() . i holds
( [a,b] in R . i iff P₁[i,a,b] )
let i be Element of F₁(); :: thesis: for a, b being Element of F₂() . i holds
( [a,b] in R . i iff P₁[i,a,b] )
let a, b be Element of F₂() . i; :: thesis: ( [a,b] in R . i iff P₁[i,a,b] )
A4: [a,b] `2 = b ;
A5: [a,b] in [:(F<sub>2</sub>() . i),(F<sub>2</sub>() . i):] by ZFMISC_1:87;
[a,b] `1 = a ;
hence ( [a,b] in R . i iff P₁[i,a,b] ) by A2, A4, A5; :: thesis: verum