consider L being Sequence such that
A1: dom L = NAT and
A2: for B being Ordinal
for L1 being Sequence st B in NAT & L1 = L | B holds
L . B = F₁(L1) from ORDINAL1:sch 4();
take L ; :: thesis: ( dom L = NAT & ( for n being Nat holds L . n = F₁((L | n)) ) )
thus dom L = NAT by A1; :: thesis: for n being Nat holds L . n = F₁((L | n))
let n be Nat; :: thesis: L . n = F₁((L | n))
reconsider B = n as Ordinal ;
B in NAT by ORDINAL1:def 12;
then L . B = F₁((L | B)) by A2;
hence L . n = F₁((L | n)) ; :: thesis: verum