take c ; :: thesis: ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & c = c )
take c ; :: thesis: ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & c = c )
take f ; :: thesis: ( <*c,f*> = x `2 & c = c )
thus ( <*c,f*> = x `2 & c = c ) by A1, MCART_1:7; :: thesis: verum