reconsider g = f as PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL by Th6;
reconsider H = ProjPMap1 (g,x) as PartFunc of (ElmFin (X,(n + 1))),ExtREAL ;
take H ; :: thesis: ex g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st
( f = g & H = ProjPMap1 (g,x) )
thus ex g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st
( f = g & H = ProjPMap1 (g,x) ) ; :: thesis: verum