consider p being FinSequence of F₁() such that
A4: ( dom p = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
P₁[k,p . k] ) ) from FINSEQ_1:sch 5(A1);
consider q being FinSequence of F₁() such that
A5: ( dom q = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
P₂[k,q . k] ) ) from FINSEQ_1:sch 5(A2);
consider r being FinSequence of F₁() such that
A6: ( dom r = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
P₃[k,r . k] ) ) from FINSEQ_1:sch 5(A3);
take p ; :: thesis: ex q, r being FinSequence of F₁() st
( dom p = Seg F₂() & dom q = Seg F₂() & dom r = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
( P₁[k,p . k] & ( for k being Nat st k in Seg F₂() holds
( P₂[k,q . k] & ( for k being Nat st k in Seg F₂() holds
P₃[k,r . k] ) ) ) ) ) )
take q ; :: thesis: ex r being FinSequence of F₁() st
( dom p = Seg F₂() & dom q = Seg F₂() & dom r = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
( P₁[k,p . k] & ( for k being Nat st k in Seg F₂() holds
( P₂[k,q . k] & ( for k being Nat st k in Seg F₂() holds
P₃[k,r . k] ) ) ) ) ) )
take r ; :: thesis: ( dom p = Seg F₂() & dom q = Seg F₂() & dom r = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
( P₁[k,p . k] & ( for k being Nat st k in Seg F₂() holds
( P₂[k,q . k] & ( for k being Nat st k in Seg F₂() holds
P₃[k,r . k] ) ) ) ) ) )
thus ( dom p = Seg F₂() & dom q = Seg F₂() & dom r = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
( P₁[k,p . k] & ( for k being Nat st k in Seg F₂() holds
( P₂[k,q . k] & ( for k being Nat st k in Seg F₂() holds
P₃[k,r . k] ) ) ) ) ) ) by A4, A5, A6; :: thesis: verum