let B, A 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 A1: ( 1 in B & A <> {} & 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 A2: ( dom fi = A & ( for C being Ordinal st C in A holds
fi . C = C *^ B ) ) ; :: thesis: A *^ B = sup fi
then A3: A *^ B = union (sup fi) by A1, ORDINAL2:54;

now

given C being Ordinal such that A4: sup fi = succ C ; :: thesis: contradiction
( C in sup fi & sup fi = sup (rng fi) ) by A4, ORDINAL1:10;
then consider D being Ordinal such that
A5: ( D in rng fi & C c= D ) by ORDINAL2:29;
D in sup fi by A5, ORDINAL2:27;
then ( succ D c= succ C & succ C c= succ D ) by A4, A5, ORDINAL1:33, ORDINAL2:1;
then succ C = succ D by XBOOLE_0:def 10;
then C = D by ORDINAL1:12;
then consider x being set such that
A6: ( x in dom fi & C = fi . x ) by A5, FUNCT_1:def 5;
reconsider x = x as Ordinal by A6;
A7: succ x in dom fi by A1, A2, A6, ORDINAL1:41;
then ( C = x *^ B & fi . (succ x) = (succ x) *^ B & C +^ 1 in C +^ B & (succ x) *^ B = (x *^ B) +^ B ) by A1, A2, A6, ORDINAL2:49, ORDINAL2:53;
then ( C +^ B in rng fi & sup fi in C +^ B ) by A4, A7, FUNCT_1:def 5, ORDINAL2:48;
hence contradiction by ORDINAL2:27; :: thesis: verum

end;

then sup fi is limit_ordinal by ORDINAL1:42;
hence A *^ B = sup fi by A3, ORDINAL1:def 6; :: thesis: verum