let n be Nat; :: thesis: for e being object holds (Segm (n + 1)) --> e = <%e%> ^ ((Segm n) --> e)
let e be object ; :: thesis: (Segm (n + 1)) --> e = <%e%> ^ ((Segm n) --> e)
set p = (Segm n) --> e;
set q = (Segm (n + 1)) --> e;
A1: dom ((Segm (n + 1)) --> e) = (len <%e%>) + (len ((Segm n) --> e)) by AFINSQ_1:33;
A2: for k being Nat st k in dom <%e%> holds
((Segm (n + 1)) --> e) . k = <%e%> . k

proof

let k be Nat; :: thesis: ( k in dom <%e%> implies ((Segm (n + 1)) --> e) . k = <%e%> . k )
assume A3: k in dom <%e%> ; :: thesis: ((Segm (n + 1)) --> e) . k = <%e%> . k
k in {0} by CARD_1:49, AFINSQ_1:def 4, A3;
then k = 0 ;
hence ((Segm (n + 1)) --> e) . k = <%e%> . k by FUNCOP_1:7, NAT_1:44; :: thesis: verum

end;

for k being Nat st k in dom ((Segm n) --> e) holds
((Segm (n + 1)) --> e) . ((len <%e%>) + k) = ((Segm n) --> e) . k

proof

let k be Nat; :: thesis: ( k in dom ((Segm n) --> e) implies ((Segm (n + 1)) --> e) . ((len <%e%>) + k) = ((Segm n) --> e) . k )
assume A4: k in dom ((Segm n) --> e) ; :: thesis: ((Segm (n + 1)) --> e) . ((len <%e%>) + k) = ((Segm n) --> e) . k
then A5: k + 1 < Segm (n + 1) by XREAL_1:8, NAT_1:44;
thus ((Segm n) --> e) . k = e by A4, FUNCOP_1:7
.= ((Segm (n + 1)) --> e) . (k + 1) by A5, NAT_1:44, FUNCOP_1:7
.= ((Segm (n + 1)) --> e) . ((len <%e%>) + k) by AFINSQ_1:34 ; :: thesis: verum

end;

hence (Segm (n + 1)) --> e = <%e%> ^ ((Segm n) --> e) by A1, A2, AFINSQ_1:def 3; :: thesis: verum