consider R being ManySortedSet of F1() such that
A2: for i being object st i in F1() holds
R . i = F3(i) from PBOOLE:sch 4();
 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):]
then F3(i) is Relation of (F2() . i),(F2() . i) by A1;
hence R . i is Element of bool [:(F2() . i),(F2() . i):] by A2, A3; :: thesis: verum
end;
hence ex R being ManySortedRelation of F2() st
for i being object st i in F1() holds
R . i = F3(i) by A2; :: thesis: for R1, R2 being ManySortedRelation of F2() st ( for i being object st i in F1() holds
R1 . i = F3(i) ) & ( for i being object st i in F1() holds
R2 . i = F3(i) ) holds
R1 = R2
let R1, R2 be ManySortedRelation of F2(); :: thesis: ( ( for i being object st i in F1() holds
R1 . i = F3(i) ) & ( for i being object st i in F1() holds
R2 . i = F3(i) ) implies R1 = R2 )
assume that
A4: for i being object st i in F1() holds
R1 . i = F3(i) and
A5: for i being object st i in F1() holds
R2 . i = F3(i) ; :: thesis: R1 = R2
now :: thesis: for i being object st i in F1() holds
R1 . i = R2 . i
let i be object ; :: thesis: ( i in F1() implies R1 . i = R2 . i )
assume A6: i in F1() ; :: thesis: R1 . i = R2 . i
then R1 . i = F3(i) by A4;
hence R1 . i = R2 . i by A5, A6; :: thesis: verum
end;
hence R1 = R2 ; :: thesis: verum