reconsider K = F₁() --> F₃(), J = F₁() --> F₂() as non-Empty Poset-yielding ManySortedSet of F₁() ;

A3: now

let X be Subset of (product K); :: thesis: ( P₁[X, product K] implies for i being Element of F₁() holds P₁[ pi X,i,K . i] )
assume A4: P₁[X, product K] ; :: thesis: for i being Element of F₁() holds P₁[ pi X,i,K . i]
let i be Element of F₁(); :: thesis: P₁[ pi X,i,K . i]
K . i = F₃() by FUNCOP_1:13;
hence P₁[ pi X,i,K . i] by A1, A4; :: thesis: verum

end;

A5: now

let i be Element of F₁(); :: thesis: for X being Subset of (K . i) st P₁[X,K . i] holds
K . i inherits_inf_of X,J . i
let X be Subset of (K . i); :: thesis: ( P₁[X,K . i] implies K . i inherits_inf_of X,J . i )
assume A6: P₁[X,K . i] ; :: thesis: K . i inherits_inf_of X,J . i
A7: J . i = F₂() by FUNCOP_1:13;
K . i = F₃() by FUNCOP_1:13;
hence K . i inherits_inf_of X,J . i by A2, A6, A7; :: thesis: verum

end;

A8: now

let i be Element of F₁(); :: thesis: K . i is full SubRelStr of J . i
J . i = F₂() by FUNCOP_1:13;
hence K . i is full SubRelStr of J . i by FUNCOP_1:13; :: thesis: verum

end;

for X being Subset of (product K) st P₁[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 (F₃() |^ F₁()) st P₁[X,F₃() |^ F₁()] holds
F₃() |^ F₁() inherits_inf_of X,F₂() |^ F₁() ; :: thesis: verum