let A be finite Ordinal-Sequence; :: thesis: A . 0 c= Sum^ A
defpred S₁[ finite T-Sequence] means for A being finite Ordinal-Sequence st $1 = A holds
A . 0 c= Sum^ A;
dom {} = {} ;
then {} . 0 = 0 by FUNCT_1:def 4;
then A0: S₁[ {} ] by XBOOLE_1:2;
A1: for f being finite T-Sequence
for x being set st S₁[f] holds
S₁[f ^ <%x%>]

proof

let f be finite T-Sequence; :: thesis: for x being set st S₁[f] holds
S₁[f ^ <%x%>]
let x be set ; :: thesis: ( S₁[f] implies S₁[f ^ <%x%>] )
assume A2: S₁[f] ; :: thesis: S₁[f ^ <%x%>]
let g be finite Ordinal-Sequence; :: thesis: ( f ^ <%x%> = g implies g . 0 c= Sum^ g )
consider b being ordinal number such that
A3: rng g c= b by ORDINAL2:def 8;
assume A4: g = f ^ <%x%> ; :: thesis: g . 0 c= Sum^ g
then rng g = (rng f) \/ (rng <%x%>) by AFINSQ_1:29;
then A5: ( rng f c= b & rng <%x%> c= b ) by A3, XBOOLE_1:11;
then reconsider f9 = f as finite Ordinal-Sequence by ORDINAL2:def 8;
rng <%x%> = {x} by AFINSQ_1:36;
then x in b by A5, ZFMISC_1:37;
then reconsider x = x as Ordinal ;

per cases ( f = {} or f <> {} ) ;

suppose f = {} ; :: thesis: g . 0 c= Sum^ g

then g = <%x%> by A4, AFINSQ_1:32;
then ( g . 0 = x & Sum^ g = x ) by Th51, AFINSQ_1:def 5;
hence g . 0 c= Sum^ g ; :: thesis: verum

end;

suppose f <> {} ; :: thesis: g . 0 c= Sum^ g

then ( 0 in dom f9 & Sum^ g = (Sum^ f9) +^ x ) by A4, Th59, ORDINAL3:10;
then ( g . 0 = f9 . 0 & f9 . 0 c= Sum^ f9 & Sum^ f9 c= Sum^ g ) by A2, A4, ORDINAL3:27, ORDINAL4:def 1;
hence g . 0 c= Sum^ g by XBOOLE_1:1; :: thesis: verum

end;

end;

end;

for f being finite T-Sequence holds S₁[f] from AFINSQ_1:sch 3(A0, A1);
hence A . 0 c= Sum^ A ; :: thesis: verum