reconsider K = F1() --> F3(), J = F1() --> F2() as non-Empty Poset-yielding ManySortedSet of F1() ;
A3:
for X being Subset of (product K) st P1[X, product K] holds
for i being Element of F1() holds P1[ pi (X,i),K . i]
by A1;
A5:
for i being Element of F1()
for X being Subset of (K . i) st P1[X,K . i] holds
K . i inherits_inf_of X,J . i
by A2;
A8:
for i being Element of F1() holds K . i is full SubRelStr of J . i
;
for X being Subset of (product K) st P1[X, product K] holds
product K inherits_inf_of X, product J
from YELLOW16:sch 3(A3, A8, A5);
hence
for X being Subset of (F3() |^ F1()) st P1[X,F3() |^ F1()] holds
F3() |^ F1() inherits_inf_of X,F2() |^ F1()
; verum