let L be non empty RelStr ; :: thesis: for N being non empty NetStr over L
for x being Element of L holds (x "/\") * N = x "/\" N
let N be non empty NetStr over L; :: thesis: for x being Element of L holds (x "/\") * N = x "/\" N
let x be Element of L; :: thesis: (x "/\") * N = x "/\" N
set n = the mapping of N;
A1: RelStr(# the carrier of ((x "/\") * N), the InternalRel of ((x "/\") * N) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def8
.= RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) by WAYBEL_2:def 3 ;
A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) by WAYBEL_2:def 3;
then reconsider f2 = the mapping of (x "/\" N) as Function of the carrier of N, the carrier of L ;
A3: for c being Element of N holds ((x "/\") * the mapping of N) . c = f2 . c
proof
let c be Element of N; :: thesis: ((x "/\") * the mapping of N) . c = f2 . c
consider y being Element of L such that
A4: y = the mapping of N . c and
A5: f2 . c = x "/\" y by A2, WAYBEL_2:def 3;
thus ((x "/\") * the mapping of N) . c = (x "/\") . y by A4, FUNCT_2:15
.= f2 . c by A5, WAYBEL_1:def 18 ; :: thesis: verum
end;
the mapping of ((x "/\") * N) = (x "/\") * the mapping of N by Def8
.= the mapping of (x "/\" N) by A3, FUNCT_2:63 ;
hence (x "/\") * N = x "/\" N by A1; :: thesis: verum