take f ; :: thesis: ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `3_3 & f = f )
take c ; :: thesis: ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `3_3 & f = f )
take f ; :: thesis: ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `3_3 & f = f )
take b ; :: thesis: ( <*c,f,b*> = x `3_3 & f = f )
thus ( <*c,f,b*> = x `3_3 & f = f ) by A1, RECDEF_2:def 3; :: thesis: verum