let x, y, z be object ; :: thesis: for f being Function st z in dom f holds
Ext (<*(f . z)*>,x,y) = <*((Ext (f,x,y)) . z)*>
let f be Function; :: thesis: ( z in dom f implies Ext (<*(f . z)*>,x,y) = <*((Ext (f,x,y)) . z)*> )
assume A1: z in dom f ; :: thesis: Ext (<*(f . z)*>,x,y) = <*((Ext (f,x,y)) . z)*>
A2: 1 in Seg 1 ;
A3: ( dom (Ext (<*(f . z)*>,x,y)) = dom <*(f . z)*> & dom <*(f . z)*> = Seg 1 ) by Def5, FINSEQ_1:38;
then A4: ( len (Ext (<*(f . z)*>,x,y)) = len <*(f . z)*> & len <*(f . z)*> = 1 ) by FINSEQ_3:29, FINSEQ_1:40;
A5: <*(f . z)*> . 1 = f . z ;

per cases ( x in f . z or not x in f . z ) ;

suppose x in f . z ; :: thesis: Ext (<*(f . z)*>,x,y) = <*((Ext (f,x,y)) . z)*>

then ( (Ext (<*(f . z)*>,x,y)) . 1 = (f . z) \/ {y} & (f . z) \/ {y} = (Ext (f,x,y)) . z ) by A2, Def5, A3, A5, A1;
hence Ext (<*(f . z)*>,x,y) = <*((Ext (f,x,y)) . z)*> by A4, FINSEQ_1:40; :: thesis: verum

end;

suppose not x in f . z ; :: thesis: Ext (<*(f . z)*>,x,y) = <*((Ext (f,x,y)) . z)*>

then ( (Ext (<*(f . z)*>,x,y)) . 1 = f . z & f . z = (Ext (f,x,y)) . z ) by A2, Def5, A3, A5, A1;
hence Ext (<*(f . z)*>,x,y) = <*((Ext (f,x,y)) . z)*> by A4, FINSEQ_1:40; :: thesis: verum

end;

end;