let f1, f2 be Function of Omega,REAL; :: thesis: ( ( for w being Element of Omega holds f1 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ) & ( for w being Element of Omega holds f2 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ) implies f1 = f2 )

assume that

A1: for w being Element of Omega holds f1 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w and

A2: for w being Element of Omega holds f2 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ; :: thesis: f1 = f2

let w be Element of Omega; :: according to FUNCT_2:def 8 :: thesis: f1 . w = f2 . w

( f1 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w & f2 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ) by A1, A2;

hence f1 . w = f2 . w ; :: thesis: verum

assume that

A1: for w being Element of Omega holds f1 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w and

A2: for w being Element of Omega holds f2 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ; :: thesis: f1 = f2

let w be Element of Omega; :: according to FUNCT_2:def 8 :: thesis: f1 . w = f2 . w

( f1 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w & f2 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ) by A1, A2;

hence f1 . w = f2 . w ; :: thesis: verum