A1: ex R being 1-sorted st
( R = F1 . i & (Carrier F1) . i = the carrier of R ) by PRALG_1:def 15;
ex R2 being 1-sorted st
( R2 = F2 . i & (Carrier F2) . i = the carrier of R2 ) by PRALG_1:def 15;
hence phi . i is Function of (F1 . i),(F2 . i) by A1, PBOOLE:def 15; :: thesis: verum