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 INSTALG1:10, INSTALG1:11;
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 A1, A2, A3, GRFUNC_1:2; :: according to AOFA_A00:def 8 :: thesis: verum