let f1, f2 be Ordinal-Sequence; :: thesis: ( f1 is increasing & f2 is increasing implies ex phi being Ordinal-Sequence st
( phi = f1 * f2 & phi is increasing ) )
assume that
A1: f1 is increasing and
A2: f2 is increasing ; :: thesis: ex phi being Ordinal-Sequence st
( phi = f1 * f2 & phi is increasing )
reconsider f = f1 * f2 as Ordinal-Sequence by A2, Th12;
take f ; :: thesis: ( f = f1 * f2 & f is increasing )
thus f = f1 * f2 ; :: thesis: f is increasing
let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b₁ being set holds
( not A in b₁ or not b₁ in dom f or f . A in f . b₁ )
let B be Ordinal; :: thesis: ( not A in B or not B in dom f or f . A in f . B )
assume that
A3: A in B and
A4: B in dom f ; :: thesis: f . A in f . B
reconsider A1 = f2 . A, B1 = f2 . B as Ordinal ;
A5: B1 in dom f1 by A4, FUNCT_1:11;
dom f c= dom f2 by RELAT_1:25;
then A6: A1 in B1 by A2, A3, A4;
A7: f . B = f1 . B1 by A4, FUNCT_1:12;
f . A = f1 . A1 by A3, A4, FUNCT_1:12, ORDINAL1:10;
hence f . A in f . B by A1, A6, A5, A7; :: thesis: verum