deffunc H₁( Nat) -> Element of the carrier of K = Det (R . $1);
consider p being FinSequence of K such that
A1: len p = len R and
A2: for i being Nat st i in dom p holds
p . i = H₁(i) from FINSEQ_2:sch 1();
take p ; :: thesis: ( dom p = dom R & ( for i being Nat st i in dom p holds
p . i = Det (R . i) ) )
thus ( dom p = dom R & ( for i being Nat st i in dom p holds
p . i = Det (R . i) ) ) by A1, A2, FINSEQ_3:29; :: thesis: verum