let A, B be Ordinal; :: thesis: ( 1 in B & A <> {} & A is limit_ordinal implies for fi being Ordinal-Sequence st dom fi = A & ( for C being Ordinal st C in A holds
fi . C = C *^ B ) holds
A *^ B = sup fi )
assume that
A1: 1 in B and
A2: A <> {} and
A3: A is limit_ordinal ; :: thesis: for fi being Ordinal-Sequence st dom fi = A & ( for C being Ordinal st C in A holds
fi . C = C *^ B ) holds
A *^ B = sup fi
let fi be Ordinal-Sequence; :: thesis: ( dom fi = A & ( for C being Ordinal st C in A holds
fi . C = C *^ B ) implies A *^ B = sup fi )
assume that
A4: dom fi = A and
A5: for C being Ordinal st C in A holds
fi . C = C *^ B ; :: thesis: A *^ B = sup fi

now :: thesis: for C being Ordinal holds not sup fi = succ C

given C being Ordinal such that A6: sup fi = succ C ; :: thesis: contradiction
consider D being Ordinal such that
A7: D in rng fi and
A8: C c= D by A6, ORDINAL1:6, ORDINAL2:21;
D in sup fi by A7, ORDINAL2:19;
then A9: succ D c= succ C by A6, ORDINAL1:21;
succ C c= succ D by A8, ORDINAL2:1;
then succ C = succ D by A9;
then C = D by ORDINAL1:7;
then consider x being object such that
A10: x in dom fi and
A11: C = fi . x by A7, FUNCT_1:def 3;
reconsider x = x as Ordinal by A10;
A12: C = x *^ B by A4, A5, A10, A11;
C +^ 1 in C +^ B by A1, ORDINAL2:32;
then A13: sup fi in C +^ B by A6, ORDINAL2:31;
A14: (succ x) *^ B = (x *^ B) +^ B by ORDINAL2:36;
A15: succ x in dom fi by A3, A4, A10, ORDINAL1:28;
then fi . (succ x) = (succ x) *^ B by A4, A5;
then C +^ B in rng fi by A15, A12, A14, FUNCT_1:def 3;
hence contradiction by A13, ORDINAL2:19; :: thesis: verum

end;

then A16: sup fi is limit_ordinal by ORDINAL1:29;
A *^ B = union (sup fi) by A2, A3, A4, A5, ORDINAL2:37;
hence A *^ B = sup fi by A16; :: thesis: verum