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 13

case 1 = {} ; :: thesis:

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

end;

case 1 <> {} ; :: 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:10; :: 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:63; :: thesis:

end;

end;