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

proof

let i be set ; :: according to MSUALG_4:def 2 :: 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):]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in R . i or x in [:(F₂() . i),(F₂() . i):] )
thus ( not x in R . i or x in [:(F₂() . i),(F₂() . i):] ) by A2, A3; :: thesis: verum

end;

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] )
( [a,b] `1 = a & [a,b] `2 = b & [a,b] in [:(F₂() . i),(F₂() . i):] ) by MCART_1:7, ZFMISC_1:106;
hence ( [a,b] in R . i iff P₁[i,a,b] ) by A2; :: thesis: verum