let S, E be non void Signature; :: thesis: ( E is S -extension implies for o being OperSymbol of S
for a being set
for r being Element of S
for r1 being Element of E st r = r1 & o is_of_type a,r holds
o is_of_type a,r1 )

assume S is Subsignature of E ; :: according to AOFA_L00:def 2 :: thesis: for o being OperSymbol of S
for a being set
for r being Element of S
for r1 being Element of E st r = r1 & o is_of_type a,r holds
o is_of_type a,r1

then A1: ( the carrier of S c= the carrier of E & the carrier' of S c= the carrier' of E & the ResultSort of S c= the ResultSort of E & the Arity of S c= the Arity of E ) by ;
let o be OperSymbol of S; :: thesis: for a being set
for r being Element of S
for r1 being Element of E st r = r1 & o is_of_type a,r holds
o is_of_type a,r1

let a be set ; :: thesis: for r being Element of S
for r1 being Element of E st r = r1 & o is_of_type a,r holds
o is_of_type a,r1

let r be Element of S; :: thesis: for r1 being Element of E st r = r1 & o is_of_type a,r holds
o is_of_type a,r1

let r1 be Element of E; :: thesis: ( r = r1 & o is_of_type a,r implies o is_of_type a,r1 )
assume A2: r = r1 ; :: thesis: ( not o is_of_type a,r or o is_of_type a,r1 )
assume A3: ( the Arity of S . o = a & the ResultSort of S . o = r ) ; :: according to AOFA_A00:def 8 :: thesis: o is_of_type a,r1
( dom the Arity of S = the carrier' of S & o in the carrier' of S & dom the ResultSort of S = the carrier' of S ) by FUNCT_2:def 1;
hence ( the Arity of E . o = a & the ResultSort of E . o = r1 ) by ; :: according to AOFA_A00:def 8 :: thesis: verum