let d be XFinSequence of REAL ; :: thesis: for k being Nat st len d = k + 1 holds
ex a being Real ex d1 being XFinSequence of REAL st
( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> )
let k be Nat; :: thesis: ( len d = k + 1 implies ex a being Real ex d1 being XFinSequence of REAL st
( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> ) )
assume AS: len d = k + 1 ; :: thesis: ex a being Real ex d1 being XFinSequence of REAL st
( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> )
set d1 = d | k;
set a = d . k;
reconsider d1 = d | k as XFinSequence of REAL ;
reconsider a = d . k as Real ;
take a ; :: thesis: ex d1 being XFinSequence of REAL st
( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> )
take d1 ; :: thesis: ( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> )
thus ( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> ) by AFINSQ_1:56, AS, AFINSQ_1:54, NAT_1:11; :: thesis: verum