ex A9 being Matrix of F₂(),F₃(),F₁() ex B9 being Matrix of F₂(),F₄(),F₁() ex N being finite without_zero Subset of NAT st
( N c= Seg F₃() & the_rank_of F₅() = the_rank_of A9 & the_rank_of F₅() = card N & P₁[A9,B9] & Segm (A9,(Seg (card N)),N) = 1. (F₁(),(card N)) & ( for i being Nat st i in dom A9 & i > card N holds
Line (A9,i) = F₃() |-> (0. F₁()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A9) & j < (Sgm N) . i holds
A9 * (i,j) = 0. F₁() ) )

A1: P₁[F₅(),F₆()] and
A2: for A9 being Matrix of F₂(),F₃(),F₁()
for B9 being Matrix of F₂(),F₄(),F₁() st P₁[A9,B9] holds
for a being Element of F₁()
for i, j being Nat st j in dom A9 & ( i = j implies a <> - (1_ F₁()) ) holds
P₁[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),F₇(B9,i,j,a)]