scheme :: MATRIX15:sch 1
GAUSS1{ F₁() -> Field, F₂() -> Nat, F₃() -> Nat, F₄() -> Nat, F₅() -> Matrix of F₂(),F₃(),F₁(), F₆() -> Matrix of F₂(),F₄(),F₁(), F₇( Matrix of F₂(),F₄(),F₁(), Nat, Nat, Element of F₁()) -> Matrix of F₂(),F₄(),F₁(), P₁[ set , set ] } :

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) is diagonal & ( for i being Nat st i in Seg (card N) holds
A9 * (i,((Sgm N) /. i)) <> 0. F₁() ) & ( 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₁() ) )

provided

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 i, j being Nat st i <> j & j in dom A9 holds
for a being Element of F₁() holds P₁[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),F₇(B9,i,j,a)]