let A be Ordinal; :: thesis:
assume A1: A <> {} ; :: thesis:
let fi be Ordinal-Sequence; :: thesis:
assume that
A2: dom fi = A and
A3: for B being Ordinal st B in A holds
fi . B = exp (1,B) ; :: thesis:

per cases ;
:: according to ORDINAL2:def 9

case 1 = 0 ; :: thesis:

hence ex b₁ being set st
( b₁ in dom fi & ( for b₂ being set holds
( not b₁ c= b₂ or not b₂ in dom fi or fi . b₂ = 0 ) ) ) ; :: thesis:

end;

case 1 <> 0 ; :: thesis:

let A1, A2 be Ordinal; :: thesis:
assume that
A4: A1 in 1 and
A5: 1 in A2 ; :: thesis:
take B = {} ; :: thesis:
thus B in dom fi by A1, A2, ORDINAL3:8; :: thesis:
let D be Ordinal; :: thesis:
assume that
B c= D and
A6: D in dom fi ; :: thesis:
exp (1,D) = fi . D by A2, A3, A6;
hence ( A1 in fi . D & fi . D in A2 ) by A4, A5, ORDINAL2:46; :: thesis:

end;

end;